Deepak Kapur - Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties

lmcs:8693 - Logical Methods in Computer Science, March 14, 2023, Volume 19, Issue 1 - https://doi.org/10.46298/lmcs-19(1:19)2023
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic PropertiesArticle

Authors: Deepak Kapur

    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.


    Volume: Volume 19, Issue 1
    Published on: March 14, 2023
    Accepted on: January 18, 2023
    Submitted on: November 10, 2021
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • AF: Small: Comprehensive Groebner, Parametric GCD Computations and Real Geometric Reasoning; Funder: National Science Foundation; Code: 1908804

    Consultation statistics

    This page has been seen 1205 times.
    This article's PDF has been downloaded 200 times.