<div class="csl-bib-body">
<div class="csl-entry">van der Giessen, I., Jalali, R., & Kuznets, R. (2023). Extensions of K5: Proof Theory and Uniform Lyndon Interpolation. In D. R. S. Ramanayake & J. Urban (Eds.), <i>Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings</i> (pp. 263–282). Springer. https://doi.org/10.1007/978-3-031-43513-3_15</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/189852
-
dc.description.abstract
We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for K5, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.
en
dc.description.sponsorship
FWF Fonds zur Förderung der wissenschaftlichen Forschung (FWF)
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Uniform interpolation
en
dc.subject
Modal logicSequent calculi
en
dc.subject
Sequent calculi
en
dc.title
Extensions of K5: Proof Theory and Uniform Lyndon Interpolation
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.contributor.affiliation
University of Birmingham, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
Utrecht University, Netherlands (the)
-
dc.contributor.editoraffiliation
Czech Technical University in Prague, Czechia
-
dc.relation.isbn
978-3-031-43513-3
-
dc.relation.doi
10.1007/978-3-031-43513-3
-
dc.relation.issn
0302-9743
-
dc.description.startpage
263
-
dc.description.endpage
282
-
dc.relation.grantno
P 33600-N
-
dc.rights.holder
Iris van der Giessen, Raheleh Jalali, and Roman Kuznets
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
dc.publisher.place
Cham
-
tuw.booktitle
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings
-
tuw.container.volume
14278
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
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.publisher.doi
10.1007/978-3-031-43513-3_15
-
dc.identifier.libraryid
AC17203332
-
dc.description.numberOfPages
20
-
tuw.author.orcid
0000-0002-3321-8087
-
tuw.author.orcid
0000-0001-5894-8724
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.editor.orcid
0000-0002-7940-9065
-
tuw.event.name
TABLEAUX 2023: 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
en
dc.description.sponsorshipexternal
UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’
-
dc.description.sponsorshipexternal
Netherlands Organization for Scientific Research
-
dc.description.sponsorshipexternal
Czech Science Foundation Grant
-
dc.relation.grantnoexternal
MR/S035540/1
-
dc.relation.grantnoexternal
639.073.807
-
dc.relation.grantnoexternal
22-06414L
-
tuw.event.startdate
18-09-2023
-
tuw.event.enddate
21-09-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Prague
-
tuw.event.country
CZ
-
tuw.event.institution
Czech Technical University in Prague
-
tuw.event.presenter
van der Giessen, Iris
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
dc.relation.isnewversionof
https://doi.org/10.48550/arXiv.2307.11727
-
item.mimetype
application/pdf
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.grantfulltext
open
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
item.fulltext
with Fulltext
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.grantno
P 33600-N
-
crisitem.author.dept
Utrecht University
-
crisitem.author.dept
Utrecht University
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems
