On the computational content of intuitionistic propositional proofs.

Kód výsledku v IS VaVaI

RIV/67985840:_____/01:05010047 - isvavai.cz

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_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

BA - Obecná matematika

OECD FORD obor

—

Projekt

IAA1019901: Matematická logika a výpočetní složitost

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ů

Název periodika

Annals of Pure and Applied Logic. Special issue

ISSN

0168-0072

e-ISSN

—

Svazek periodika

109

Číslo periodika v rámci svazku

1-2

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

16

Strana od-do

49-64

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—