Recommendations
Cites work
- scientific article; zbMATH DE number 1614687 (Why is no real title available?)
- scientific article; zbMATH DE number 5542185 (Why is no real title available?)
- scientific article; zbMATH DE number 1903346 (Why is no real title available?)
- scientific article; zbMATH DE number 1903356 (Why is no real title available?)
- scientific article; zbMATH DE number 2090300 (Why is no real title available?)
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- An algorithm for reasoning about equality
- Computer Aided Verification
- Computer Aided Verification
- Efficiency of a Good But Not Linear Set Union Algorithm
- Fast Decision Procedures Based on Congruence Closure
- Justifying equality
- Mechanizing Mathematical Reasoning
- Shostak's congruence closure as completion
- Term Rewriting and Applications
- Theorem proving using lazy proof explication.
- Tools and Algorithms for the Construction and Analysis of Systems
- Validated proof-producing decision procedures
- Variations on the Common Subexpression Problem
Cited in
(31)- Verifying Whiley programs with Boogie
- Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
- Conditional congruence closure over uninterpreted and interpreted symbols
- An automata view to goal-directed methods
- Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR
- Deciding confluence and normal form properties of ground term rewrite systems efficiently
- Computing congruent closures on terms
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- Fault-tolerant aggregate signatures
- scientific article; zbMATH DE number 1614687 (Why is no real title available?)
- Congruence closure with free variables
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Fast LCF-Style Proof Reconstruction for Z3
- Congruence closure with integer offsets
- Congruence closure in intensional type theory
- Satisfiability modulo theories
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Justifying equality
- Invariant neural architecture for learning term synthesis in instantiation proving
- Extending SMT solvers to higher-order logic
- New
- Theory exploration powered by deductive synthesis
- NP-completeness of small conflict set generation for congruence closure
- Abstract congruence closure
- Model-based theory combination
- Modal tableau systems with blocking and congruence closure
- Congruence classes with logic variables
- 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
This page was built for publication: Fast congruence closure and extensions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q876046)
