On extracting computations from propositional proofs
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F10%3A00422140" target="_blank" >RIV/67985840:_____/10:00422140 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.30" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.30</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2010.30" target="_blank" >10.4230/LIPIcs.FSTTCS.2010.30</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
On extracting computations from propositional proofs
Popis výsledku v původním jazyce
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 usedto 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.
Název v anglickém jazyce
On extracting computations from propositional proofs
Popis výsledku anglicky
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 usedto 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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
BA - Obecná matematika
OECD FORD obor
—
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2010
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
ISBN
978-3-939897-23-1
ISSN
—
e-ISSN
—
Počet stran výsledku
12
Strana od-do
30-41
Název nakladatele
Schloss Dagstuhl, Leibniz-Zentrum für Informatik
Místo vydání
Wadem
Místo konání akce
Chennai
Datum konání akce
15. 12. 2010
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
000310361000003