Extracting verified decision procedures: DPLL and resolution

DOI10.2168/LMCS-11(1:6)2015MaRDI QIDQ5177337zbMATH OpenFDO

Authors Ulrich Berger, Andrew Lawrence, Fredrik Nordvall Forsberg, Monika Seisenberger

Publication date 11 March 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1502.02131

zbMATH Keywords

DPLLinteractive theorem provingprogram extractionSAT

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Extracting a DPLL algorithm
• Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
• Extracting the resolution algorithm from a completeness proof for the propositional calculus
• The mechanical verification of a DPLL-based satisfiability solver
• scientific article; zbMATH DE number 5713654

Cited in

(5)

• Verifying the conversion into CNF in dafny
• Extracting a DPLL algorithm
• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
• Extracting the resolution algorithm from a completeness proof for the propositional calculus

Describes a project that uses

Uses Software

• versat
• Idris
• Metis
• LLVM
• Chaff
• Sledgehammer
• Agda
• Minlog
• MiniSat
• Coq
• Isabelle/HOL

This page was built for publication: Extracting verified decision procedures: DPLL and resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5177337)