Conditional congruence closure over uninterpreted and interpreted symbols

DOI10.1007/S11424-019-8377-8zbMath1417.68077OpenAlexW2911667399WikidataQ128393049 ScholiaQ128393049MaRDI QIDQ1730315

Deepak Kapur

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

zbMATH Keywords

completionrewritingcongruence closureconditional congruence closureintepreted symbolsuninterpreted symbols

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (6)

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

• RRL

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

This page was built for publication: Conditional congruence closure over uninterpreted and interpreted symbols