Generalizing DPLL and satisfiability for equalities

DOI10.1016/J.IC.2007.03.003zbMATH Open1121.68102DBLPjournals/iandc/BadbanPTZ07OpenAlexW2157688865WikidataQ62047491 ScholiaQ62047491MaRDI QIDQ2643080FDOQ2643080

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

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)\)

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Title not available (Why is that?)
• Computer Aided Verification
• Title not available (Why is that?)
• Equational problems and disunification
• Generalizing DPLL and satisfiability for equalities
• Solvable cases of the decision problem
• Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\).
• Algebraic process verification.
• Mechanizing Mathematical Reasoning
• Title not available (Why is that?)
• Title not available (Why is that?)
• Congruence closure with integer offsets
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the complexity of equational problems in CNF
• Zero, successor and equality in BDDs
• BDD based procedures for a theory of equality with uninterpreted functions
• Transforming equality logic to propositional logic
• Artificial Intelligence and Symbolic Computation

Cited In (9)

• Generalizing DPLL and satisfiability for equalities
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Computer Aided Verification
• Generalizing DPLL to Richer Logics

Uses Software

• ATERM
• CVC
• ICS
• mCRL

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)