Canonized Rewriting and Ground AC Completion Modulo Shostak Theories

DOI10.1007/978-3-642-19835-9_6zbMATH Open1315.68219arXiv1207.3262OpenAlexW2101824738MaRDI QIDQ3000635FDOQ3000635

Authors: Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala 

Publication date: 19 May 2011

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

Abstract: AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm for the word problem. In this paper, we present a modular extension of ground AC-completion for deciding formulas in the combination of the theory of equality with user-defined AC symbols, uninterpreted symbols and an arbitrary signature disjoint Shostak theory X. Our algorithm, called AC(X), is obtained by augmenting in a modular way ground AC-completion with the canonizer and solver present for the theory X. This integration rests on canonized rewriting, a new relation reminiscent to normalized rewriting, which integrates canonizers in rewriting steps. AC(X) is proved sound, complete and terminating, and is implemented to extend the core of the Alt-Ergo theorem prover.

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

Recommendations

• Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation
• Coalgebraic Completeness-via-Canonicity
• Rewriting in the partial algebra of typed terms modulo AC
• Generalized rewrite theories and coherence completion
• Generalized rewrite theories, coherence completion, and symbolic methods
• AC-complete unification and its application to theorem proving
• Modular proofs for completeness of hierarchical term rewriting systems
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Consistency and Completeness of Rewriting in the Calculus of Constructions
• Finite canonical rewriting systems for congruences generated by concurrency relations

zbMATH Keywords

commutativityrewritingdecision procedureSMT solversassociativityShostak'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)

Cites Work

• Simplification by Cooperating Decision Procedures
• Orderings for term-rewriting systems
• Term Rewriting and All That
• Title not available (Why is that?)
• Complete Sets of Reductions for Some Equational Theories
• Rewriting Techniques and Applications
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Title not available (Why is that?)
• Shostak's congruence closure as completion
• Deciding Combinations of Theories
• Completion of a Set of Rules Modulo a Set of Equations
• A total AC-compatible ordering based on RPO
• Abstract congruence closure
• Canonization for disjoint unions of theories
• Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation

Cited In (4)

• Any ground associative-commutative theory has a finite canonical system
• Building Extended Canonizers by Graph-Based Deduction
• Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation
• On ground AC-completion

Uses Software

• Alt-Ergo

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

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