<div class="csl-bib-body">
<div class="csl-entry">Girlando, M., Kuznets, R., Marin, S., Morales, M., & Straßburger, L. (2023, September 27). <i>Intuitionistic S4 and its decidability</i> [Conference Presentation]. Mosaic Workshop 2023, Wien, Austria. http://hdl.handle.net/20.500.12708/192652</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192652
-
dc.description.abstract
We present a decision procedure for IS4, an intuitionistic modal logic first formulated by Fisher Servi. The logic has two independent modalities and is interpreted over birelational Kripke models. Unlike other intuitionistic modal logics, the problem of decidability of IS4 has been open for almost thirty years, since it has been posed in Simpson’s PhD thesis in 1994. Our result is obtained by defining a proof-search algorithm based on a labelled sequent calculus that explicitly incorporates the two accessibility relations of Kripke models for the logic. The search algorithm outputs either a proof or a finite countermodel, thus additionally establishing the finite model property for IS4.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.subject
decidability
en
dc.subject
Intuitionistic modal logic
en
dc.subject
labeled proof systems
en
dc.title
Intuitionistic S4 and its decidability
en
dc.type
Presentation
en
dc.type
Vortrag
de
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.grantno
P 33600-N
-
dc.type.category
Conference Presentation
-
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-9384-1356
-
tuw.author.orcid
0000-0001-5894-8724
-
tuw.author.orcid
0000-0003-4661-6540
-
tuw.event.name
Mosaic Workshop 2023
-
tuw.event.startdate
26-09-2023
-
tuw.event.enddate
29-09-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Wien
-
tuw.event.country
AT
-
tuw.event.institution
RISE-MSCA
-
tuw.event.presenter
Kuznets, Roman
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cp
-
item.openairetype
conference paper not in proceedings
-
item.languageiso639-1
en
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.grantno
P 33600-N
-
crisitem.author.dept
University of Amsterdam
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems
