Generalizing DPLL to Richer Logics

DOI10.1007/978-3-642-02658-4_35MaRDI QIDQ3636877zbMATH OpenOpenAlexFDO

Authors K. L. McMillan, Andreas Kuehlmann, Mooly Sagiv

Publication date 30 June 2009

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_35

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27)

Recommendations

• Computer Aided Verification
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Generalizing DPLL and satisfiability for equalities
• scientific article; zbMATH DE number 1931669
• Computer Aided Verification

Cited in

(15)

• Cutting to the chase.
• Generalizing DPLL and satisfiability for equalities
• A survey of satisfiability modulo theory
• Semantically-guided goal-sensitive reasoning: model representation
• Satisfiability modulo theories
• Deciding floating-point logic with abstract conflict driven clause learning
• Cutting to the chase. Solving linear integer arithmetic
• Solving systems of linear inequalities by bound propagation
• Computer Aided Verification
• Linear quantifier elimination as an abstract decision procedure
• Global guidance for local generalization in model checking
• The CDSAT method for satisfiability modulo theories and assignment: an exposition
• FMplex: a novel method for solving linear real arithmetic problems
• FMplex: exploring a bridge between Fourier-Motzkin and simplex
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs

This page was built for publication: Generalizing DPLL to Richer Logics

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