Počet záznamů: 1  

On extracting computations from propositional proofs

  1. 1.
    0422140 - MÚ 2014 RIV DE eng C - Konferenční příspěvek (zahraniční konf.)
    Pudlák, Pavel
    On extracting computations from propositional proofs.
    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.), s. 30-41. Leibniz International Proceedings in Informatics, vol. 8. ISBN 978-3-939897-23-1.
    [International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), /30./. Chennai (IN), 15.12.2010-16.12.2010]
    Grant CEP: GA AV ČR IAA100190902; GA MŠk(CZ) 1M0545
    Výzkumný záměr: CEZ:AV0Z10190503
    Klíčová slova: proof complexity * propositional tautology * boolean circuits
    Kód oboru RIV: BA - Obecná matematika

    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.
    Trvalý link: http://hdl.handle.net/11104/0228350
    Název souboruStaženoVelikostKomentářVerzePřístup
    Pudlak2.pdf1424.5 KBVydavatelský postprintpovolen
Počet záznamů: 1