Generalizing DPLL and satisfiability for equalities

DOI10.1016/J.IC.2007.03.003MaRDI QIDQ2643080zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Bahareh Badban, Jaco van de Pol, Olga Tveretina, Hans Zantema

Publication date 23 August 2007

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2007.03.003

zbMATH Keywords

decision procedureDPLL procedureequalityground term algebrainductive datatypessatisfiability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Computer Aided Verification
• Generalizing DPLL to Richer Logics
• A DPLL-based calculus for ground satisfiability modulo theories
• 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)\)

Cites work

• A Computing Procedure for Quantification Theory
• A framework for cooperating decision procedures
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A SAT based approach for solving formulas over Boolean and linear mathematical propositions
• Algebraic process verification.
• Artificial Intelligence and Symbolic Computation
• BDD based procedures for a theory of equality with uninterpreted functions
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• Combining Shostak theories
• Computer Aided Verification
• Congruence closure with integer offsets
• CVC: A cooperating validity checker
• Deciding equality formulas by small domains instantiations
• Equational binary decision diagrams
• Equational problems and disunification
• Exploiting positive equality in a logic of equality with uninterpreted functions
• FDPLL -- a first-order Davis-Putnam-Logeman-Loveland procedure
• Generalizing DPLL and satisfiability for equalities
• scientific article; zbMATH DE number 4053011 (Why is no real title available?)
• ICS: Integrated canonizer and solver
• Mechanizing Mathematical Reasoning
• On the complexity of equational problems in CNF
• Solvable cases of the decision problem
• Transforming equality logic to propositional logic
• Zero, successor and equality in BDDs

Cited in

(9)

• Generalizing DPLL and satisfiability for equalities
• FDPLL -- a first-order Davis-Putnam-Logeman-Loveland procedure
• Computing All Implied Equalities via SMT-Based Partition Refinement
• Generalized Davis-Putnam and satisfiability problems in mathematics
• Generalizing DPLL to Richer Logics
• Deciding floating-point logic with abstract conflict driven clause learning
• Deciding equality formulas by small domains instantiations
• EufDPLL -- a tool to check satisfiability of equality logic formulas
• Computer Aided Verification

Describes a project that uses

Uses Software

• ATERM
• ICS
• mCRL
• CVC

This page was built for publication: Generalizing DPLL and satisfiability for equalities

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