Modal interpolation via nested sequents

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] 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
[img]
Preview
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:

08 Sep 2017 22:21

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 Edit item
Provide Feedback