Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
From MaRDI portal
Publication:3000635
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
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
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