Fast congruence closure and extensions

DOI10.1016/j.ic.2006.08.009zbMath1112.68116OpenAlexW2138865396MaRDI QIDQ876046

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

zbMATH Keywords

verificationequational reasoningdecision procedurescongruence closure

Mathematics Subject Classification ID

Data structures (68P05)

Related Items

Theory exploration powered by deductive synthesis, Satisfiability Modulo Theories, New, Modal Tableau Systems with Blocking and Congruence Closure, NP-completeness of small conflict set generation for congruence closure, Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Conditional congruence closure over uninterpreted and interpreted symbols, Congruence Closure with Free Variables, An Automata View to Goal-Directed Methods, Unnamed Item, Fault-Tolerant Aggregate Signatures, Efficient Interpolant Generation in Satisfiability Modulo Theories, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), Extending SMT solvers to higher-order logic, 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, Model-based Theory Combination, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Verifying Whiley programs with Boogie

Uses Software

• Chaff
• MathSAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fast Decision Procedures Based on Congruence Closure
• Variations on the Common Subexpression Problem
• Efficiency of a Good But Not Linear Set Union Algorithm
• An algorithm for reasoning about equality
• Shostak's congruence closure as completion
• Computer Aided Verification
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Tools and Algorithms for the Construction and Analysis of Systems
• Term Rewriting and Applications
• Computer Aided Verification
• Mechanizing Mathematical Reasoning
• Computer Aided Verification