<div class="csl-bib-body">
<div class="csl-entry">van der Giessen, I., Jalali, R., & Kuznets, R. (2022, November 1). <i>Nested Sequents, Kripke Models, and Uniform Interpolation</i> [Conference Presentation]. Proof-theoretic and algebraic aspects of (intuitionistic) modal logics, Utrecht, Netherlands (the). http://hdl.handle.net/20.500.12708/135862</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/135862
-
dc.description.abstract
Proof-theoretic method is one of the primary sources for constructive proofs of interpolation. After first being used to prove Craig interpolation using cut-free sequent calculi, the method has been extended to Lyndon interpolation, and uniform interpolation, as well as to analytic sequent calculi. More recently, it has been extended to hypersequents, nested sequents, labelled sequents, yielding, for instance, a positive answer to the open problem of whether Gödel logic (intermediate logic of linear frames) has Lyndon interpolation.
An interesting feature of this extension is its essential use of Kripke semantics (for modal or intermediate logics). While the algorithm for contructing interpolants is purely proof-theoretic, the proof of its correctness relies on the semantics. More pertinently, the algorithm in general and individual interpolant transformations in particular are guided and shaped by the structure of Kripke models of the logic in question.
In this work, we extend this syntactico-semantic method to proving uniform interpolation for K, D, and T using nested sequents and for S5 using hypersequents.
en
dc.description.sponsorship
Fonds zur Förderung der wissenschaftlichen Forschung (FWF)
-
dc.language.iso
en
-
dc.subject
interpolation
en
dc.subject
Nested sequent
en
dc.subject
Hypersequent
en
dc.subject
modal logic
en
dc.title
Nested Sequents, Kripke Models, and Uniform Interpolation
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.contributor.affiliation
Utrecht University, Netherlands (the)
-
dc.contributor.affiliation
Utrecht University, Netherlands (the)
-
dc.relation.grantno
P 33600-N
-
dc.type.category
Conference Presentation
-
tuw.publication.invited
invited
-
tuw.project.title
Reasoning about Knowledge in Byzantine Distributed Systems
-
tuw.researchTopic.id
I2
-
tuw.researchTopic.name
Computer Engineering and Software-Intensive Systems
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E191-02 - Forschungsbereich Embedded Computing Systems
-
tuw.author.orcid
0000-0002-3321-8087
-
tuw.author.orcid
0000-0001-5894-8724
-
tuw.event.name
Proof-theoretic and algebraic aspects of (intuitionistic) modal logics
en
tuw.event.startdate
01-11-2022
-
tuw.event.enddate
01-11-2022
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Utrecht
-
tuw.event.country
NL
-
tuw.event.institution
Utrecht University
-
tuw.event.presenter
Kuznets, Roman
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.grantfulltext
none
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cp
-
item.openairetype
conference paper not in proceedings
-
item.cerifentitytype
Publications
-
item.fulltext
no Fulltext
-
item.languageiso639-1
en
-
crisitem.author.dept
University of Birmingham, UK
-
crisitem.author.dept
Utrecht University
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems
