Fast congruence closure and extensions
From MaRDI portal
Publication:876046
DOI10.1016/J.IC.2006.08.009zbMATH Open1112.68116OpenAlexW2138865396MaRDI QIDQ876046FDOQ876046
Authors: Robert Nieuwenhuis, Albert Oliveras 
Publication date: 16 April 2007
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2006.08.009
Recommendations
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Efficiency of a Good But Not Linear Set Union Algorithm
- Variations on the Common Subexpression Problem
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Computer Aided Verification
- Computer Aided Verification
- Fast Decision Procedures Based on Congruence Closure
- Theorem proving using lazy proof explication.
- Shostak's congruence closure as completion
- Mechanizing Mathematical Reasoning
- Tools and Algorithms for the Construction and Analysis of Systems
- Justifying equality
- Term Rewriting and Applications
- Title not available (Why is that?)
- Title not available (Why is that?)
- Validated proof-producing decision procedures
- An algorithm for reasoning about equality
- Title not available (Why is that?)
Cited In (31)
- Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
- Verifying Whiley programs with Boogie
- 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
- Title not available (Why is that?)
- 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
- Congruence Closure with Free Variables
- 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
Uses Software
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)
