On extracting computations from propositional proofs (a survey)

Pudlák, Pavel

doi:10.4230/LIPIcs.FSTTCS.2010.30

Document

On extracting computations from propositional proofs (a survey)

Author Pavel Pudlák

Part of: Volume: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2010-12-14

PDF

File

PDF

LIPIcs.FSTTCS.2010.30.pdf

Filesize: 414 kB
12 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSTTCS.2010.30
URN: urn:nbn:de:0030-drops-28512

Subject Classification

Keywords

proof complexity
propositional tautology
boolean circuits
resolution
feasible interpolation

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

This paper describes a project that aims at showing that propositional proofs of certain tautologies in weak proof system give upper bounds on the computational complexity of functions associated with the tautologies. Such bounds can potentially be used to prove (conditional or unconditional) lower bounds on the lengths of proofs of these tautologies and show separations of some weak proof systems. The prototype are the results showing the feasible interpolation property for resolution. In order to prove similar results for systems stronger than resolution one needs to define suitable generalizations of boolean circuits. We will survey the known results concerning this project and sketch in which direction we want to generalize them.

Cite As Get BibTex

Pavel Pudlák. On extracting computations from propositional proofs (a survey). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 30-41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.FSTTCS.2010.30

Author Details

Pavel Pudlák

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail