License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.15
URN: urn:nbn:de:0030-drops-142530
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14253/
Go to the corresponding LIPIcs Volume Portal

Kapur, Deepak

A Modular Associative Commutative (AC) Congruence Closure Algorithm

pdf-format:
LIPIcs-FSCD-2021-15.pdf (0.7 MB)

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 the 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 and/or have identities, as well as their various combinations. The 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 Satisfiability modulo Theories (SMT) solvers.

BibTeX - Entry

@InProceedings{kapur:LIPIcs.FSCD.2021.15,
  author =	{Kapur, Deepak},
  title =	{{A Modular Associative Commutative (AC) Congruence Closure Algorithm}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{15:1--15:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14253},
  URN =		{urn:nbn:de:0030-drops-142530},
  doi =		{10.4230/LIPIcs.FSCD.2021.15},
  annote =	{Keywords: Congruence Closure, Associative and Commutative, Word Problems, Finitely Presented Algebras, Equational Theories}
}

Keywords: Congruence Closure, Associative and Commutative, Word Problems, Finitely Presented Algebras, Equational Theories
Collection: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Issue Date: 2021
Date of publication: 06.07.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI