Fast congruence closure and extensions
From MaRDI portal
Publication:876046
DOI10.1016/J.IC.2006.08.009zbMATH Open1112.68116OpenAlexW2138865396MaRDI QIDQ876046FDOQ876046
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
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Computer Aided Verification
- 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
- Validated proof-producing decision procedures
- An algorithm for reasoning about equality
Cited In (23)
- Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
- Verifying Whiley programs with Boogie
- Conditional congruence closure over uninterpreted and interpreted symbols
- Modal Tableau Systems with Blocking and Congruence Closure
- Computing congruent closures on terms
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- 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
- Fault-Tolerant Aggregate Signatures
- Congruence Closure with Free Variables
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- 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
- Title not available (Why is that?)
- An Automata View to Goal-Directed Methods
- Model-based theory combination
- Satisfiability Modulo Theories
- 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)
