Canonized Rewriting and Ground AC Completion Modulo Shostak Theories

DOI10.1007/978-3-642-19835-9_6zbMath1315.68219arXiv1207.3262OpenAlexW2101824738MaRDI QIDQ3000635

Mohamed Iguernelala, Evelyne Contejean, Sylvain Conchon

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1207.3262

zbMATH Keywords

rewritingassociativitycommutativitySMT solversdecision procedureShostak's algorithmAC-completion

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Word problems, etc. in computability and recursion theory (03D40)

Uses Software

• Alt-Ergo

Cites Work

• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• A total AC-compatible ordering based on RPO
• Abstract congruence closure
• Canonization for disjoint unions of theories
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation
• Deciding Combinations of Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Simplification by Cooperating Decision Procedures
• Complete Sets of Reductions for Some Equational Theories
• Shostak's congruence closure as completion
• Term Rewriting and All That
• Rewriting Techniques and Applications