Proof Theory for Positive Logic with Weak Negation

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
Proof Theory for Positive Logic with Weak Negation
Original language description
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.
Czech name
—
Czech description
—

Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project
<a href="/en/project/GA17-04630S" target="_blank" >GA17-04630S: Predicate graded logics and their applications to computer science</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)