Number of the records: 1
Proof Theory for Positive Logic with Weak Negation
- 1.
SYSNO ASEP 0505107 Document Type J - Journal Article R&D Document Type Journal Article Subsidiary J Článek ve WOS Title Proof Theory for Positive Logic with Weak Negation Author(s) Bílková, Marta (UIVT-O) SAI, RID, ORCID
Colacito, A. (IT)Source Title Studia Logica. - : Springer - ISSN 0039-3215
Roč. 108, č. 4 (2020), s. 649-686Number of pages 38 s. Language eng - English Country NL - Netherlands Keywords Minimal propositional logic ; Weak negation ; Intuitionistic propositional logic ; Sequent calculus ; Terminating sequent calculus ; Decidability ; Complexity Subject RIV BA - General Mathematics OECD category Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8) R&D Projects GA17-04630S GA ČR - Czech Science Foundation (CSF) Method of publishing Limited access Institutional support UIVT-O - RVO:67985807 UT WOS 000549716200001 EID SCOPUS 85069155898 DOI 10.1007/s11225-019-09869-y Annotation 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. Workplace Institute of Computer Science Contact Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800 Year of Publishing 2021 Electronic address http://dx.doi.org/10.1007/s11225-019-09869-y
Number of the records: 1