Extracting the resolution algorithm from a completeness proof for the propositional calculus

&
Annals of Pure and Applied Logic 161 (3):337-348 (2010)
  Copy   BIBTEX

Abstract

We prove constructively that for any propositional formula in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of showing that it is unsatisfiable. This refutation is a resolution proof of ¬. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction. The account is an example of the genre of highly readable formalized mathematics

Categories

Keywords

Reprint years

2009

DOI

10.1016/j.apal.2009.07.008

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,369

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Minimum propositional proof length is NP-Hard to linearly approximate.Michael Alekhnovich, Sam Buss, Shlomo Moran & Toniann Pitassi - 2001 - Journal of Symbolic Logic 66 (1):171-191.
CERES in higher-order logic.Stefan Hetzl, Alexander Leitsch & Daniel Weller - 2011 - Annals of Pure and Applied Logic 162 (12):1001-1034.
Cutting planes, connectivity, and threshold logic.Samuel R. Buss & Peter Clote - 1996 - Archive for Mathematical Logic 35 (1):33-62.
The limits of tractability in Resolution-based propositional proof systems.Stefan Dantchev & Barnaby Martin - 2012 - Annals of Pure and Applied Logic 163 (6):656-668.
On the computational content of intuitionistic propositional proofs.Samuel R. Buss & Pavel Pudlák - 2001 - Annals of Pure and Applied Logic 109 (1-2):49-64.
Dual Erotetic Calculi and the Minimal LFI.Szymon Chlebowski & Dorota Leszczyńska-Jasion - 2015 - Studia Logica 103 (6):1245-1278.
Relative efficiency of propositional proof systems: resolution vs. cut-free LK.Noriko H. Arai - 2000 - Annals of Pure and Applied Logic 104 (1-3):3-16.
Pool resolution is NP-hard to recognize.Samuel R. Buss - 2009 - Archive for Mathematical Logic 48 (8):793-798.
A Resolution Calculus For Shortening Proofs.Nicolas Peltier - 2005 - Logic Journal of the IGPL 13 (3):307-333.
Intuitionistic completeness of first-order logic.Robert Constable & Mark Bickford - 2014 - Annals of Pure and Applied Logic 165 (1):164-198.

Analytics

Added to PP
2013-12-22

Downloads
30 (#757,175)

6 months
8 (#605,434)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

A Machine-Oriented Logic based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.

Add more references