Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
From MaRDI portal
Publication:6135743
DOI10.46298/LMCS-19(1:19)2023arXiv2111.04793MaRDI QIDQ6135743FDOQ6135743
Authors: Deepak Kapur 
Publication date: 26 August 2023
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/2111.04793
Recommendations
groupidempotencynilpotencycanonical formcongruence closurecancelationassociative-commutativeGröbner basiscanonical rewrite systems
Cites Work
- Variations on the Common Subexpression Problem
- Title not available (Why is that?)
- Term Rewriting and All That
- Title not available (Why is that?)
- Complete Sets of Reductions for Some Equational Theories
- New results on rewrite-based satisfiability procedures
- Normalized rewriting: An alternative to rewriting modulo a set of equations
- Fast Decision Procedures Based on Congruence Closure
- The complexity of the word problems for commutative semigroups and polynomial ideals
- Computing a Gröbner basis of a polynomial ideal over a Euclidean domain
- Only prime superpositions need be considered in the Knuth-Bendix completion procedure
- Critical pair criteria for completion
- Shostak's congruence closure as completion
- New decision algorithms for finitely presented commutative semigroups
- An algorithm for computing a Gröbner basis of a polynomial ideal over a ring with zero divisors
- On ground AC-completion
- Any ground associative-commutative theory has a finite canonical system
- Title not available (Why is that?)
- Fast congruence closure and extensions
- An algorithm for reasoning about equality
- Abstract congruence closure
- Implementing contextual rewriting
- Title not available (Why is that?)
- Conditional congruence closure over uninterpreted and interpreted symbols
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- Deciding the word problem for ground identities with commutative and extensional symbols
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)
