Modal interpolation via nested sequents. Fitting, M. & Kuznets, R. Annals of pure and applied logic, 166(3):274–305, Elsevier, March, 2015. Paper abstract bibtex 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.
@article{fkm15,
volume = {166},
number = {3},
month = {March},
author = {Melvin Fitting and Roman Kuznets},
title = {Modal interpolation via nested sequents},
publisher = {Elsevier},
year = {2015},
journal = {Annals of pure and applied logic},
pages = {274--305},
url = {2015/fkm15.pdf},
abstract = {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.}
}
Downloads: 0
{"_id":"WrnPZGw5ALST3FpAY","bibbaseid":"fitting-kuznets-modalinterpolationvianestedsequents-2015","authorIDs":[],"author_short":["Fitting, M.","Kuznets, R."],"bibdata":{"bibtype":"article","type":"article","volume":"166","number":"3","month":"March","author":[{"firstnames":["Melvin"],"propositions":[],"lastnames":["Fitting"],"suffixes":[]},{"firstnames":["Roman"],"propositions":[],"lastnames":["Kuznets"],"suffixes":[]}],"title":"Modal interpolation via nested sequents","publisher":"Elsevier","year":"2015","journal":"Annals of pure and applied logic","pages":"274–305","url":"2015/fkm15.pdf","abstract":"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.","bibtex":"@article{fkm15,\n volume = {166},\n number = {3},\n month = {March},\n author = {Melvin Fitting and Roman Kuznets},\n title = {Modal interpolation via nested sequents},\n publisher = {Elsevier},\n year = {2015},\n journal = {Annals of pure and applied logic},\n pages = {274--305},\n url = {2015/fkm15.pdf},\n abstract = {The main method of proving the Craig Interpolation Property\n (CIP) constructively uses cut-free sequent proof systems.\n Until now, however, no such method has been known for proving\n the CIP using more general sequent-like proof formalisms, such\n as hypersequents, nested sequents, and labelled sequents. In\n this paper, we start closing this gap by presenting an\n algorithm for proving the CIP for modal logics by induction\n on a nested-sequent derivation. This algorithm is applied to\n all the logics of the so-called modal cube.}\n}\n\n","author_short":["Fitting, M.","Kuznets, R."],"key":"fkm15","id":"fkm15","bibbaseid":"fitting-kuznets-modalinterpolationvianestedsequents-2015","role":"author","urls":{"Paper":"http://home.inf.unibe.ch/~brambi/2015/fkm15.pdf"},"downloads":0},"bibtype":"article","biburl":"http://home.inf.unibe.ch/~brambi/ltg.bib","creationDate":"2020-02-26T09:06:59.010Z","downloads":0,"keywords":[],"search_terms":["modal","interpolation","via","nested","sequents","fitting","kuznets"],"title":"Modal interpolation via nested sequents","year":2015,"dataSources":["jFQMeatnEb8qn3qdH"]}