Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

DOI10.2168/LMCS-8(3:16)2012zbMath1253.68291OpenAlexW3101473842MaRDI QIDQ2914237

Evelyne Contejean, Mohamed Iguernelala, Sylvain Conchon

Publication date: 25 September 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2168/lmcs-8(3:16)2012

zbMATH Keywords

rewritingSMT solversdecision procedureShostak's algorithmAC-completionassociativity and commutativity

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items (2)

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories ⋮ Order-Sorted Rewriting and Congruence Closure

Uses Software

• Alt-Ergo

This page was built for publication: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation