Disjunction-free disjunction property

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F23%3A00604291" target="_blank" >RIV/67985840:_____/23:00604291 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Disjunction-free disjunction property

Popis výsledku v původním jazyce

Frege proof systems (often called Hilbert-style systems outside proof complexity) are among the simplest and most natural proof systems for classical and nonclassical propositional logics, they are polynomially equivalent to sequent calculi and natural deduction systems, which further testifies to their robustness and fundamental status. Although it is commonly assumed for all classical propositional proof systems that some tautologies require exponentially large proofs, this has been proven so far only for relatively weak proof systems, unrestricted Frege systems are far beyond the reach of current lower bound techniques.

Název v anglickém jazyce

Disjunction-free disjunction property

Popis výsledku anglicky

Frege proof systems (often called Hilbert-style systems outside proof complexity) are among the simplest and most natural proof systems for classical and nonclassical propositional logics, they are polynomially equivalent to sequent calculi and natural deduction systems, which further testifies to their robustness and fundamental status. Although it is commonly assumed for all classical propositional proof systems that some tautologies require exponentially large proofs, this has been proven so far only for relatively weak proof systems, unrestricted Frege systems are far beyond the reach of current lower bound techniques.

Druh

O - Ostatní výsledky

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

<a href="/cs/project/GA23-04825S" target="_blank" >GA23-04825S: Logika a nesplnitelnost</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2023

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ů