Conditional congruence closure over uninterpreted and interpreted symbols
From MaRDI portal
Publication:1730315
DOI10.1007/s11424-019-8377-8zbMath1417.68077OpenAlexW2911667399WikidataQ128393049 ScholiaQ128393049MaRDI QIDQ1730315
Publication date: 6 March 2019
Published in: Journal of Systems Science and Complexity (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s11424-019-8377-8
completionrewritingcongruence closureconditional congruence closureintepreted symbolsuninterpreted symbols
Related Items
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ Foreword to the special issue ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Unnamed Item ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols ⋮ Deciding the word problem for ground identities with commutative and extensional symbols
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Constraint solving for interpolation
- Fast congruence closure and extensions
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
- New decision algorithms for finitely presented commutative semigroups
- Abstract congruence closure
- On interpolation in automated theorem proving
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Completion of a Set of Rules 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
- Efficiency of a Good But Not Linear Set Union Algorithm
- An algorithm for reasoning about equality
- Shostak's congruence closure as completion
- On Shostak's decision procedure for combinations of theories
- Term Rewriting and All That
- Canonical Ground Horn Theories
- Any ground associative-commutative theory has a finite canonical system
- An improved equivalence algorithm
- Cover Algorithms and Their Combination
- Implementing contextual rewriting
