Extracting verified decision procedures : DPLL and resolution

Berger, Ulrich and Lawrence, Andrew and Nordvall Forsberg, Fredrik and Seisenberger, Monika (2015) Extracting verified decision procedures : DPLL and resolution. Logical Methods in Computer Science, 11 (1). 6. ISSN 1860-5974

[img]
Preview
 Text (Berger-etal-LMCS-2015-Extracting-verified-decision-procedures-DPLL-and-resolution)
Berger_etal_LMCS_2015_Extracting_verified_decision_procedures_DPLL_and_resolution.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (200kB)| Preview

    Abstract

    This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation showing its unsatisfiability. We use non-computational quantifiers to remove redundant computational content from the extracted program and translate it into Haskell to improve performance. We also prove the equivalence between the resolution proof system and the DPLL proof system with a bound on the size of the resulting resolution proof. This demonstrates that it is possible to capture quantitative information about the extracted program on the proof level. The formalization is carried out in the interactive proof assistant Minlog.

    Author(s):Berger, Ulrich, Lawrence, Andrew, Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288 and Seisenberger, Monika
    Item type:Article
    ID code:52996
    Keywords:program extraction, verification tools, DPLL proof system, Computer software, Computer Science(all), Theoretical Computer Science
    Subjects:Science > Mathematics > Computer software
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:13 May 2015 09:55
    Last modified:25 Jan 2020 04:30
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/52996
    Export data:
    CORE (COnnecting REpositories)