Deciding effectively propositional logic using DPLL and substitution sets (Q972432)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Deciding effectively propositional logic using DPLL and substitution sets
scientific article

    Statements

    Deciding effectively propositional logic using DPLL and substitution sets (English)
    0 references
    0 references
    0 references
    0 references
    26 May 2010
    0 references
    This paper introduces a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also called EPR. This class of first-order formulas provides a generalization of pure propositional satisfiablility and quantified Boolean formulas. The presented DPLL calculus is complete in EPR and combines techniques for efficient propositional search, such as Binary Decision Diagrams. The calculus works directly at the level of sets and it is opened up to efficient implementations based on data structures, with promising preliminary empirical results.
    0 references
    DPLL
    0 references
    SAT
    0 references
    BDDS
    0 references
    effectively propositional logic
    0 references
    0 references
    0 references

    Identifiers