Fast Decision Procedures Based on Congruence Closure
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A view of computability on term algebras
- A linear time solution to the single function coarsest partition problem
- An algebraic semantics approach to the effective resolution of type equations
- A decision procedure for combinations of propositional temporal logic and other specialized theories
- A structure-preserving clause form translation
- The Church-Rosser property for ground term-rewriting systems is decidable
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
- On the relationship of congruence closure and unification
- Unification theory
- Complexity, convexity and combinations of theories
- Algebraic specifiability of data types with minimal computable parameters
- Inferring the equivalence of functional programs that mutate data
- A fast algorithm for constructing a tree automaton recognizing a congruential tree language
- Embedding complex decision procedures inside an interactive theorem prover.
- A first order logic of effects
- Deciding the word problem in the union of equational theories.
- A rewriting approach to satisfiability procedures.
- Constraint contextual rewriting.
- NP-completeness of small conflict set generation for congruence closure
- Conditional congruence closure over uninterpreted and interpreted symbols
- Parallelizing SMT solving: lazy decomposition and conciliation
- Zero, successor and equality in BDDs
- Algorithms and reductions for rewriting problems. II.
- Deciding confluence of certain term rewriting systems in polynomial time
- On rewriting rules in Mizar
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
- Efficient automated reasoning about sets and multisets with cardinality constraints
- Deciding the word problem for ground identities with commutative and extensional symbols
- 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
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Incremental search for conflict and unit instances of quantified formulas with E-matching
- From LCF to Isabelle/HOL
- Extending SMT solvers to higher-order logic
- Strategies for combining decision procedures
- Decision procedures for term algebras with integer constraints
- A taxonomy of exact methods for partial Max-SAT
- Embedded software verification using symbolic execution and uninterpreted functions
- Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages
- Fault-tolerant aggregate signatures
- Order-Sorted Rewriting and Congruence Closure
- Congruence closure in intensional type theory
- Colors Make Theories Hard
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Meta-programming with built-in type equality
- Conjunctive abstract interpretation using paramodulation
- Proving properties of functional programs by equality saturation
- On interpolation in decision procedures
- Congruence closure of compressed terms in polynomial time
- Satisfiability modulo theories
- Congruence closure with free variables
- Inductive prover based on equality saturation for a lazy functional language
- Modal tableau systems with blocking and congruence closure
- Efficient algorithms for bounded rigid E-unification
- Ground Interpolation for the Theory of Equality
- Combining decision procedures by (model-)equality propagation
- \(E\)-unification with constants vs. general \(E\)-unification
- Deciding confluence and normal form properties of ground term rewrite systems efficiently
- Algebraic data integration
- On quasitautologies
- A framework for using knowledge in tableau proofs
- Cyclic connections
- On Shostak's decision procedure for combinations of theories
- Variant-Based Satisfiability in Initial Algebras
- MACE4 and SEM: a comparison of finite model generators
- Combining non-stably infinite theories
- Equivalence in functional languages with effects
- Analysis of the equality relations for the program terms
- Efficient ground completion
- Solving equation systems in ω-categorical algebras
- A term rewriting technique for decision graphs
- Combining Decision Procedures by (Model-)Equality Propagation
- 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
- A language for generic programming in the large
- An Improved Tight Closure Algorithm for Integer Octagonal Constraints
- Generalized partial computation using disunification to solve constraints
- SCL(EQ): SCL for first-order logic with equality
- Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Even Faster Conflicts and Lazier Reductions for String Solvers
- Trace Abstraction-Based Verification for Uninterpreted Programs
- KBO Constraint Solving Revisited
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Incremental dead state detection in logarithmic time
- Transforming optimization problems into disciplined convex programming form
- Complete axiomatizations of some quotient term algebras
- Another variation on the common subexpression problem
- Computing ground congruence classes
- Interoperability of proof systems with SC-TPTP
- Producing and verifying extremely large propositional refutations
- Congruence closure modulo groups
- Model completeness for rational trees
- A lazy and modular approach to int-blasting
- Modular derivation of decision procedures for extensions of the algebraic theory of arrays
- Pattern-directed invocation with changing equations
This page was built for publication: Fast Decision Procedures Based on Congruence Closure
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3883564)
