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

satisfiabilityequalitydecision procedureinductive datatypesDPLL procedureground term algebra

Mathematics Subject Classification ID

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

Recommendations

• Computer Aided Verification
• Generalizing DPLL to Richer Logics
• scientific article; zbMATH DE number 1931669
• 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

• scientific article; zbMATH DE number 1614688 (Why is no real title available?)
• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• scientific article; zbMATH DE number 1696764 (Why is no real title available?)
• scientific article; zbMATH DE number 4053011 (Why is no real title available?)
• scientific article; zbMATH DE number 1798183 (Why is no real title available?)
• scientific article; zbMATH DE number 1903374 (Why is no real title available?)
• scientific article; zbMATH DE number 2090060 (Why is no real title available?)
• scientific article; zbMATH DE number 2090300 (Why is no real title available?)
• scientific article; zbMATH DE number 2102726 (Why is no real title available?)
• scientific article; zbMATH DE number 2102727 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A machine program for theorem-proving
• 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)\).
• Computer Aided Verification
• Congruence closure with integer offsets
• Equational problems and disunification
• Generalizing DPLL and satisfiability for equalities
• 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 to Richer Logics
• Generalizing DPLL and satisfiability for equalities
• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• Deciding floating-point logic with abstract conflict driven clause learning
• EufDPLL -- a tool to check satisfiability of equality logic formulas
• Computing All Implied Equalities via SMT-Based Partition Refinement
• Generalized Davis-Putnam and satisfiability problems in mathematics
• scientific article; zbMATH DE number 2102726 (Why is no real title available?)
• Computer Aided Verification

Describes a project that uses

Uses Software

• mCRL
• ICS
• CVC
• ATERM

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)