Proof Theory for Positive Logic with Weak Negation

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F20%3A00505107" target="_blank" >RIV/67985807:_____/20:00505107 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/s11225-019-09869-y" target="_blank" >http://dx.doi.org/10.1007/s11225-019-09869-y</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s11225-019-09869-y" target="_blank" >10.1007/s11225-019-09869-y</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Proof Theory for Positive Logic with Weak Negation

Popis výsledku v původním jazyce

Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is proved, and used to conclude that the considered logical systems are PSPACE-complete.

Název v anglickém jazyce

Proof Theory for Positive Logic with Weak Negation

Popis výsledku anglicky

Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is proved, and used to conclude that the considered logical systems are PSPACE-complete.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA17-04630S" target="_blank" >GA17-04630S: Predikátové škálované logiky a jejich aplikace v informatice</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2020

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

Studia Logica

ISSN

0039-3215

e-ISSN

—

Svazek periodika

108

Číslo periodika v rámci svazku

4

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

38

Strana od-do

649-686

Kód UT WoS článku

000549716200001

EID výsledku v databázi Scopus

2-s2.0-85069155898