On the computational content of intuitionistic propositional proofs.

Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F01%3A05010047" target="_blank" >RIV/67985840:_____/01:05010047 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—

Jazyk výsledku
angličtina
Název v původním jazyce
On the computational content of intuitionistic propositional proofs.
Popis výsledku v původním jazyce
The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Hornclosure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs.
Název v anglickém jazyce
On the computational content of intuitionistic propositional proofs.
Popis výsledku anglicky
The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Hornclosure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs.

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
<a href="/cs/project/IAA1019901" target="_blank" >IAA1019901: Matematická logika a výpočetní složitost</a><br>
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění
2001
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)