Bílková, Marta; Colacito, Almudena (2020). Proof theory for positive logic with weak negation. Studia logica, 108(4), pp. 649-686. Springer Science + Business Media 10.1007/s11225-019-09869-y
|
Text
B_lkov_-Colacito2020_Article_ProofTheoryForPositiveLogicWit.pdf - Published Version Available under License Publisher holds Copyright. Download (692kB) | Preview |
|
Text
1907.05411.pdf - Submitted Version Restricted to registered users only Available under License Publisher holds Copyright. Download (270kB) |
Proof-theoreticmethods 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.
Item Type: |
Journal Article (Original Article) |
---|---|
Division/Institute: |
08 Faculty of Science > Department of Mathematics and Statistics > Institute of Mathematics |
UniBE Contributor: |
Colacito, Almudena |
Subjects: |
500 Science > 510 Mathematics |
ISSN: |
0039-3215 |
Publisher: |
Springer Science + Business Media |
Language: |
English |
Submitter: |
Sebastiano Don |
Date Deposited: |
10 Feb 2021 17:06 |
Last Modified: |
26 Jul 2023 00:25 |
Publisher DOI: |
10.1007/s11225-019-09869-y |
ArXiv ID: |
1907.05411 |
Uncontrolled Keywords: |
Minimal propositional logic, Weak negation, Intuitionistic propositional logic, Sequent calculus, Terminating sequent calculus, Decidability, Complexity |
BORIS DOI: |
10.48350/151262 |
URI: |
https://boris.unibe.ch/id/eprint/151262 |