No Cover Image

Journal article 1691 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!
first_indexed 2015-07-06T02:09:51Z
last_indexed 2019-07-17T20:20:28Z
id cronfa22264
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-07-17T15:15:17.3081190</datestamp><bib-version>v2</bib-version><id>22264</id><entry>2015-07-06</entry><title>Extracting verified decision procedures: DPLL and Resolution</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>d035399b2b324a63fe472ce0344653e0</sid><ORCID>0000-0002-2226-386X</ORCID><firstname>Monika</firstname><surname>Seisenberger</surname><name>Monika Seisenberger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2015-07-06</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Logical Methods in Computer Science</journal><volume>11</volume><journalNumber>1</journalNumber><publisher/><keywords>DPLL, Program Extraction, Interactive Theorem Proving, SAT</keywords><publishedDay>10</publishedDay><publishedMonth>3</publishedMonth><publishedYear>2015</publishedYear><publishedDate>2015-03-10</publishedDate><doi>10.2168/LMCS-11(1:6)2015</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-07-17T15:15:17.3081190</lastEdited><Created>2015-07-06T00:12:09.5281475</Created><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author><author><firstname>Andrew</firstname><surname>Lawrence</surname><order>2</order></author><author><firstname>Fredrik Nordvall</firstname><surname>Forsberg</surname><order>3</order></author><author><firstname>Monika</firstname><surname>Seisenberger</surname><orcid>0000-0002-2226-386X</orcid><order>4</order></author></authors><documents><document><filename>0022264-06062017230121.pdf</filename><originalFilename>Seisenberger-ExtractingVerifiedDecisionProcedures-LMCS.pdf</originalFilename><uploaded>2017-06-06T23:01:21.8530000</uploaded><type>Output</type><contentLength>229227</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><embargoDate>2017-06-06T00:00:00.0000000</embargoDate><documentNotes>CC licence</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2019-07-17T15:15:17.3081190 v2 22264 2015-07-06 Extracting verified decision procedures: DPLL and Resolution 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false d035399b2b324a63fe472ce0344653e0 0000-0002-2226-386X Monika Seisenberger Monika Seisenberger true false 2015-07-06 SCS 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. Journal Article Logical Methods in Computer Science 11 1 DPLL, Program Extraction, Interactive Theorem Proving, SAT 10 3 2015 2015-03-10 10.2168/LMCS-11(1:6)2015 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2019-07-17T15:15:17.3081190 2015-07-06T00:12:09.5281475 Ulrich Berger 0000-0002-7677-3582 1 Andrew Lawrence 2 Fredrik Nordvall Forsberg 3 Monika Seisenberger 0000-0002-2226-386X 4 0022264-06062017230121.pdf Seisenberger-ExtractingVerifiedDecisionProcedures-LMCS.pdf 2017-06-06T23:01:21.8530000 Output 229227 application/pdf Version of Record true 2017-06-06T00:00:00.0000000 CC licence true eng
title Extracting verified decision procedures: DPLL and Resolution
spellingShingle Extracting verified decision procedures: DPLL and Resolution
Ulrich Berger
Monika Seisenberger
title_short Extracting verified decision procedures: DPLL and Resolution
title_full Extracting verified decision procedures: DPLL and Resolution
title_fullStr Extracting verified decision procedures: DPLL and Resolution
title_full_unstemmed Extracting verified decision procedures: DPLL and Resolution
title_sort Extracting verified decision procedures: DPLL and Resolution
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
d035399b2b324a63fe472ce0344653e0
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
d035399b2b324a63fe472ce0344653e0_***_Monika Seisenberger
author Ulrich Berger
Monika Seisenberger
author2 Ulrich Berger
Andrew Lawrence
Fredrik Nordvall Forsberg
Monika Seisenberger
format Journal article
container_title Logical Methods in Computer Science
container_volume 11
container_issue 1
publishDate 2015
institution Swansea University
doi_str_mv 10.2168/LMCS-11(1:6)2015
document_store_str 1
active_str 0
description 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.
published_date 2015-03-10T03:26:30Z
_version_ 1763750959464316928
score 11.037319

Similar Items