Engineering DPLL(T) + Saturation

DOI10.1007/978-3-540-71070-7_40zbMath1165.68479OpenAlexW1595962583MaRDI QIDQ3541724

Nikolaj Bjørner, Leonardo de Moura

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_40

Mathematics Subject Classification ID

Related Items (19)

Semantically-guided goal-sensitive reasoning: model representation ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Quantifier simplification by unification in SMT ⋮ Superposition Modulo Non-linear Arithmetic ⋮ Superposition as a decision procedure for timed automata ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Congruence Closure with Free Variables ⋮ Simple and Efficient Clause Subsumption with Feature Vector Indexing ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Combinable Extensions of Abelian Groups ⋮ Fault-Tolerant Aggregate Signatures ⋮ Superposition Modulo Linear Arithmetic SUP(LA) ⋮ Data Structures with Arithmetic Constraints: A Non-disjoint Combination ⋮ Theory decision by decomposition ⋮ SMELS: satisfiability modulo equality with lazy superposition

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• E-matching for Fun and Profit
• Solving SAT and SAT Modulo Theories
• Labelled Splitting
• Simplify: a theorem prover for program checking
• Integrating Linear Arithmetic into Superposition Calculus
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Substitution tree indexing
• New results on rewrite-based satisfiability procedures
• Automated Reasoning

This page was built for publication: Engineering DPLL(T) + Saturation