Generalizing DPLL and satisfiability for equalities

DOI10.1016/j.ic.2007.03.003zbMath1121.68102OpenAlexW2157688865WikidataQ62047491 ScholiaQ62047491MaRDI QIDQ2643080

Jaco van de Pol, Bahareh Badban, 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

Related Items (3)

Generalizing DPLL and satisfiability for equalities ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

Uses Software

• ATERM
• CVC
• ICS
• mCRL

Cites Work

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

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