Proofs with monotone cuts

Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F12%3A00377738" target="_blank" >RIV/67985840:_____/12:00377738 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1002/malq.201020071" target="_blank" >http://dx.doi.org/10.1002/malq.201020071</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1002/malq.201020071" target="_blank" >10.1002/malq.201020071</a>

Jazyk výsledku
angličtina
Název v původním jazyce
Proofs with monotone cuts
Popis výsledku v původním jazyce
Atserias, Galesi, and Pudlak have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK (or equivalently, in Frege systems). We generalize the simulation to the fragment MCLKof LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.
Název v anglickém jazyce
Proofs with monotone cuts
Popis výsledku anglicky
Atserias, Galesi, and Pudlak have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK (or equivalently, in Frege systems). We generalize the simulation to the fragment MCLKof LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.

Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
BA - Obecná matematika
OECD FORD obor
—

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>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění
2012
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ů

Podobné výsledky(10)