Fitting, Melvin; Kuznets, Roman (2015). Modal interpolation via nested sequents. Annals of pure and applied logic, 166(3), pp. 274-305. Elsevier 10.1016/j.apal.2014.11.002
![[img]](https://boris.unibe.ch/style/images/fileicons/text.png) |
Text
1-s2.0-S0168007214001183-main.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (692kB) | Request a copy |
|
|
Text
kuznets - interpolation.pdf - Accepted Version Available under License Publisher holds Copyright. Download (469kB) | Preview |
The main method of proving the Craig Interpolation Property (CIP) constructively uses cut-free sequent proof systems. Until now, however, no such method has been known for proving the CIP using more general sequent-like proof formalisms, such as hypersequents, nested sequents, and labelled sequents. In this paper, we start closing this gap by presenting an algorithm for proving the CIP for modal logics by induction on a nested-sequent derivation. This algorithm is applied to all the logics of the so-called modal cube.
Item Type: |
Journal Article (Original Article) |
|---|---|
Division/Institute: |
08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG) 08 Faculty of Science > Institute of Computer Science (INF) |
UniBE Contributor: |
Kuznets, Roman |
Subjects: |
000 Computer science, knowledge & systems 500 Science > 510 Mathematics |
ISSN: |
0168-0072 |
Publisher: |
Elsevier |
Language: |
English |
Submitter: |
Lukas Jaun |
Date Deposited: |
06 Aug 2015 15:43 |
Last Modified: |
05 Dec 2022 14:48 |
Publisher DOI: |
10.1016/j.apal.2014.11.002 |
BORIS DOI: |
10.7892/boris.70699 |
URI: |
https://boris.unibe.ch/id/eprint/70699 |
Actions (login required)
 |
Edit item |