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