Abstract congruence closure

DOI10.1023/B:JARS.0000009518.26415.49zbMath1040.03006MaRDI QIDQ1425161

Laurent Vigneron, Leo Bachmair, Ashish Kumar Tiwari

Publication date: 15 March 2004

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

term rewritingcongruence closureassociative-commutative theories

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Strategies for combining decision procedures, Deciding confluence of certain term rewriting systems in polynomial time, Theorem Proving with Bounded Rigid E-Unification, Modal Tableau Systems with Blocking and Congruence Closure, Efficient Algorithms for Bounded Rigid E-unification, Compositional Specification in Rewriting Logic, Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Conditional congruence closure over uninterpreted and interpreted symbols, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, Canonical Ground Horn Theories, Order-Sorted Rewriting and Congruence Closure, Congruence Closure in Intensional Type Theory, Combination of convex theories: modularity, deduction completeness, and explanation, Deduction, Strategies, and Rewriting, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Rewrite-Based Satisfiability Procedures for Recursive Data Structures