Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation

DOI10.2168/LMCS-8(3:16)2012zbMATH Open1253.68291OpenAlexW3101473842MaRDI QIDQ2914237FDOQ2914237

Authors: Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala 

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

Recommendations

• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• Rewriting in the partial algebra of typed terms modulo AC
• AC-complete unification and its application to theorem proving
• Generalized rewrite theories, coherence completion, and symbolic methods
• Coalgebraic Completeness-via-Canonicity
• Generalized rewrite theories and coherence completion
• Modular proofs for completeness of hierarchical term rewriting systems
• scientific article; zbMATH DE number 2079835
• A total, ground path ordering for proving termination of AC-rewrite systems
• Termination proofs for ground rewrite systems -- interpretations and derivational complexity

zbMATH Keywords

rewritingdecision procedureSMT solversShostak's algorithmAC-completionassociativity and commutativity

Mathematics Subject Classification ID

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

Cited In (4)

• Any ground associative-commutative theory has a finite canonical system
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• On ground AC-completion
• 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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914237)