Number of the records: 1

On extracting computations from propositional proofs

SYSNO ASEP	0422140
Document Type	C - Proceedings Paper (int. conf.)
R&D Document Type	Conference Paper
Title	On extracting computations from propositional proofs
Author(s)	Pudlák, Pavel (MU-W)_{RID, SAI}
Source Title	IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. - Wadem : Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2010 / Lodaya K. ; Mahajan M - ISBN 978-3-939897-23-1
Pages	s. 30-41
Number of pages	12 s.
Publication form	Print - P
Action	International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), /30./
Event date	15.12.2010-16.12.2010
VEvent location	Chennai
Country	IN - India
Event type	WRD
Language	eng - English
Country	DE - Germany
Keywords	proof complexity ; propositional tautology ; boolean circuits
Subject RIV	BA - General Mathematics
R&D Projects	IAA100190902 GA AV ČR - Academy of Sciences of the Czech Republic (AV ČR)
	1M0545 GA MŠMT - Ministry of Education, Youth and Sports (MEYS)
CEZ	AV0Z10190503 - MU-W (2005-2011)
UT WOS	000310361000003
EID SCOPUS	84880199880
DOI	10.4230/LIPIcs.FSTTCS.2010.30
Annotation	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.
Workplace	Mathematical Institute
Contact	Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757
Year of Publishing	2014

Number of the records: 1