About: On the computational content of intuitionistic propositional proofs.

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: On the computational content of intuitionistic propositional proofs. Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	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 Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. 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 Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. (en)
Title	On the computational content of intuitionistic propositional proofs. On the computational content of intuitionistic propositional proofs. (en)
skos:prefLabel	On the computational content of intuitionistic propositional proofs. On the computational content of intuitionistic propositional proofs. (en)
skos:notation	RIV/67985840:_____/01:05010047!RIV/2003/AV0/A05003/N
http://linked.open.../vavai/riv/strany	49;64
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(IAA1019901), Z(AV0Z1019905)
http://linked.open...iv/cisloPeriodika	1-2
http://linked.open...vai/riv/dodaniDat	2003
http://linked.open...aciTvurceVysledku	Pudlák, Pavel
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Matematický ústav AV ČR, v. v. i.
http://linked.open...dnocenehoVysledku	689968
http://linked.open...ai/riv/idVysledku	RIV/67985840:_____/01:05010047
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	N/A (en)
http://linked.open.../riv/klicoveSlovo	N/A
http://linked.open...odStatuVydavatele	NL - Nizozemsko
http://linked.open...ontrolniKodProRIV	[A5120B87B4E9]
http://linked.open...i/riv/nazevZdroje	Annals of Pure and Applied Logic. Special issue
http://linked.open...in/vavai/riv/obor	BA
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...ocetUcastnikuAkce	0 (xsd:int)
http://linked.open...nichUcastnikuAkce	0 (xsd:int)
http://linked.open...vavai/riv/projekt	Mathematical logic and computational complexity
http://linked.open...UplatneniVysledku	2001
http://linked.open...v/svazekPeriodika	109
http://linked.open...iv/tvurceVysledku	Pudlák, Pavel Buss, S. R.
http://linked.open...n/vavai/riv/zamer	Complex development of all branches of mathematics with regard to the needs of physics and technology
issn	0168-0072
number of pages	16 (xsd:int)

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 48 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software