Fast Decision Procedures Based on Congruence Closure
From MaRDI portal
Publication:3883564
DOI10.1145/322186.322198zbMath0441.68111OpenAlexW2153131284MaRDI QIDQ3883564
Publication date: 1980
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322186.322198
congruence closuredecision procedure quantifier-free theory of equalityquantifier-free theory of LISP list structuretheory of recursive data types
Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items (93)
Generalized partial computation using disunification to solve constraints ⋮ Theory exploration powered by deductive synthesis ⋮ Strategies for combining decision procedures ⋮ Deciding confluence of certain term rewriting systems in polynomial time ⋮ Proving properties of functional programs by equality saturation ⋮ Congruence Closure of Compressed Terms in Polynomial Time ⋮ An algebraic semantics approach to the effective resolution of type equations ⋮ Satisfiability Modulo Theories ⋮ Efficient ground completion ⋮ Inductive Prover Based on Equality Saturation for a Lazy Functional Language ⋮ Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness ⋮ Modal Tableau Systems with Blocking and Congruence Closure ⋮ Efficient Algorithms for Bounded Rigid E-unification ⋮ A decision procedure for combinations of propositional temporal logic and other specialized theories ⋮ A structure-preserving clause form translation ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ The Church-Rosser property for ground term-rewriting systems is decidable ⋮ Fast algorithms for testing unsatisfiability of ground Horn clauses with equations ⋮ Fast congruence closure and extensions ⋮ On the relationship of congruence closure and unification ⋮ Unification theory ⋮ Algebraic data integration ⋮ A first order logic of effects ⋮ NP-completeness of small conflict set generation for congruence closure ⋮ Complexity, convexity and combinations of theories ⋮ Deciding the word problem in the union of equational theories. ⋮ A rewriting approach to satisfiability procedures. ⋮ Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Conjunctive Abstract Interpretation Using Paramodulation ⋮ Constraint contextual rewriting. ⋮ On rewriting rules in Mizar ⋮ Decision procedures for term algebras with integer constraints ⋮ A taxonomy of exact methods for partial Max-SAT ⋮ Combining decision procedures by (model-)equality propagation ⋮ \(E\)-unification with constants vs. general \(E\)-unification ⋮ Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages ⋮ On quasitautologies ⋮ A framework for using knowledge in tableau proofs ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems ⋮ Rigid E-unification: NP-completeness and applications to equational matings ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Algebraic specifiability of data types with minimal computable parameters ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Congruence Closure with Free Variables ⋮ On Interpolation in Decision Procedures ⋮ Cyclic connections ⋮ On Shostak's decision procedure for combinations of theories ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Inferring the equivalence of functional programs that mutate data ⋮ Complete axiomatizations of some quotient term algebras ⋮ Another variation on the common subexpression problem ⋮ MACE4 and SEM: A Comparison of Finite Model Generators ⋮ Solving equation systems in ω-categorical algebras ⋮ Combining Non-Stably Infinite Theories ⋮ A language for generic programming in the large ⋮ Producing and verifying extremely large propositional refutations ⋮ A Term Rewriting Technique for Decision Graphs ⋮ Combining Decision Procedures by (Model-)Equality Propagation ⋮ Zero, successor and equality in BDDs ⋮ Unnamed Item ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Equivalence in functional languages with effects ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ From LCF to Isabelle/HOL ⋮ Embedded software verification using symbolic execution and uninterpreted functions ⋮ Fault-Tolerant Aggregate Signatures ⋮ An Improved Tight Closure Algorithm for Integer Octagonal Constraints ⋮ Ground Interpolation for the Theory of Equality ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ A fast algorithm for constructing a tree automaton recognizing a congruential tree language ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Congruence Closure in Intensional Type Theory ⋮ Colors Make Theories Hard ⋮ Extending SMT solvers to higher-order logic ⋮ A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method ⋮ A practical integration of first-order reasoning and decision procedures ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols ⋮ A view of computability on term algebras ⋮ Efficient automated reasoning about sets and multisets with cardinality constraints ⋮ Deciding the word problem for ground identities with commutative and extensional symbols ⋮ Algorithms and reductions for rewriting problems. II. ⋮ CC(X): Semantic Combination of Congruence Closure with Solvable Theories ⋮ An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Verifying Whiley programs with Boogie ⋮ Fast left Kan extensions using the chase ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ A linear time solution to the single function coarsest partition problem ⋮ Meta-programming With Built-in Type Equality ⋮ Pattern-directed invocation with changing equations ⋮ Analysis of the equality relations for the program terms
This page was built for publication: Fast Decision Procedures Based on Congruence Closure
