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

DOI10.2168/LMCS-8(3:16)2012MaRDI QIDQ2914237zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(4)

• Any ground associative-commutative theory has a finite canonical system
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• Order-Sorted Rewriting and Congruence Closure
• On ground AC-completion

Describes a project that uses

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)