<div class="csl-bib-body">
<div class="csl-entry">Girlando, M., Kuznets, R., Marin, S., Morales, M., & Straßburger, L. (2023). Intuitionistic S4 is decidable. In <i>2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)</i>. LICS 2023: Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, Boston, MA, United States of America (the). IEEE. https://doi.org/10.34726/5295</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/190629
-
dc.identifier.uri
https://doi.org/10.34726/5295
-
dc.description.abstract
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area.
en
dc.description.sponsorship
FWF Fonds zur Förderung der wissenschaftlichen Forschung (FWF)
-
dc.language.iso
en
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
intuitionistic modal logic
en
dc.subject
labeled proof systems
en
dc.subject
decidability
en
dc.title
Intuitionistic S4 is decidable
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.identifier.doi
10.34726/5295
-
dc.contributor.affiliation
University of Amsterdam, Netherlands (the)
-
dc.contributor.affiliation
University of Birmingham, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
Inria Saclay - Île-de-France Research Centre, France
-
dc.contributor.affiliation
Inria Saclay - Île-de-France Research Centre, France
-
dc.relation.isbn
9798350335873
-
dc.relation.grantno
P 33600-N
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
-
tuw.relation.publisher
IEEE
-
tuw.relation.publisherplace
Piscataway
-
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.linking
https://doi.org/10.48550/arXiv.2304.12094
-
tuw.publication.orgunit
E191-02 - Forschungsbereich Embedded Computing Systems
-
tuw.publisher.doi
10.1109/LICS56636.2023.10175684
-
dc.identifier.libraryid
AC17205016
-
dc.description.numberOfPages
29
-
tuw.author.orcid
0000-0002-9384-1356
-
tuw.author.orcid
0000-0001-5894-8724
-
tuw.author.orcid
0000-0003-4661-6540
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.event.name
LICS 2023: Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science
-
dc.description.sponsorshipexternal
Horizon 2021 programme, under the Marie Skłodowska-Curie grant CYDER
-
dc.relation.grantnoexternal
101064105
-
tuw.event.startdate
26-06-2023
-
tuw.event.enddate
29-06-2023
-
tuw.event.online
Hybrid
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Boston, MA
-
tuw.event.country
US
-
tuw.event.institution
Boston University
-
tuw.event.presenter
Straßburger, Lutz
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
mixedopen
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
crisitem.author.dept
University of Amsterdam
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems
