Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
From MaRDI portal
Publication:6135743
Abstract: Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing a congruence closure by abstracting nonflat terms by constants as proposed first in Kapur's congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency, identities, cancellativity and group properties as well as their various combinations. Algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into the Satisfiability modulo Theories (SMT) solvers. A new way to view Groebner basis algorithm for polynomial ideals with integer coefficients as a combination of the congruence closures over the AC symbol * with the identity 1 and the congruence closure over an Abelian group with + is outlined.
Recommendations
Cites work
- scientific article; zbMATH DE number 3896290 (Why is no real title available?)
- scientific article; zbMATH DE number 1538018 (Why is no real title available?)
- scientific article; zbMATH DE number 217454 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- Abstract congruence closure
- An algorithm for computing a Gröbner basis of a polynomial ideal over a ring with zero divisors
- An algorithm for reasoning about equality
- Any ground associative-commutative theory has a finite canonical system
- Complete Sets of Reductions for Some Equational Theories
- Computing a Gröbner basis of a polynomial ideal over a Euclidean domain
- Conditional congruence closure over uninterpreted and interpreted symbols
- Critical pair criteria for completion
- Deciding the word problem for ground identities with commutative and extensional symbols
- Fast Decision Procedures Based on Congruence Closure
- Fast congruence closure and extensions
- Implementing contextual rewriting
- New decision algorithms for finitely presented commutative semigroups
- New results on rewrite-based satisfiability procedures
- Normalized rewriting: An alternative to rewriting modulo a set of equations
- On ground AC-completion
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Shostak's congruence closure as completion
- Term Rewriting and All That
- The complexity of the word problems for commutative semigroups and polynomial ideals
- Variations on the Common Subexpression Problem
This page was built for publication: Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135743)
