A DPLL-based calculus for ground satisfiability modulo theories

DOI10.1007/3-540-45757-7_26MaRDI QIDQ4708927zbMATH OpenFDO

Authors Cesare Tinelli

Publication date 20 June 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2424/24240308.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27)

Recommendations

• Logic for Programming, Artificial Intelligence, and Reasoning
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• A model-constructing satisfiability calculus
• Engineering DPLL(T) + Saturation
• Computer Aided Verification

Cited in

(18)

• A framework for satisfiability modulo theories
• Twenty years of rewriting logic
• Automated generation of exam sheets for automated deduction
• Strategies for combining decision procedures
• The model evolution calculus as a first-order DPLL method
• Generalizing DPLL and satisfiability for equalities
• A model-constructing satisfiability calculus
• Satisfiability modulo theories
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Engineering DPLL(T) + Saturation
• Generalizing DPLL to Richer Logics
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• Logic for Programming, Artificial Intelligence, and Reasoning
• Computer Aided Verification
• The model evolution calculus.
• First order Büchi automata and their application to verification of LTL specifications
• Finding connections via satisfiability solving
• Deciding effectively propositional logic using DPLL and substitution sets

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: A DPLL-based calculus for ground satisfiability modulo theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4708927)