No Cover Image

Journal article 1690 views 145 downloads

Extracting verified decision procedures: DPLL and Resolution

Ulrich Berger Orcid Logo, Andrew Lawrence, Fredrik Nordvall Forsberg, Monika Seisenberger Orcid Logo

Logical Methods in Computer Science, Volume: 11, Issue: 1

Swansea University Authors: Ulrich Berger Orcid Logo, Monika Seisenberger Orcid Logo

DOI (Published version): 10.2168/LMCS-11(1:6)2015

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...

Full description

Published in: Logical Methods in Computer Science
Published: 2015
URI: https://cronfa.swan.ac.uk/Record/cronfa22264
Tags: Add Tag
No Tags, Be the first to tag this record!
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.
Keywords: DPLL, Program Extraction, Interactive Theorem Proving, SAT
Issue: 1

Similar Items