Canonized Rewriting and Ground AC Completion Modulo Shostak Theories

DOI10.1007/978-3-642-19835-9_6MaRDI QIDQ3000635zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cites work

• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• 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
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Deciding Combinations of Theories
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Orderings for term-rewriting systems
• Rewriting Techniques and Applications
• Shostak's congruence closure as completion
• Simplification by Cooperating Decision Procedures
• Term Rewriting and All That

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

Describes a project that uses

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)