Satisfiability vs. Finite Satisfiability in Elementary Modal Logics

We study elementary modal logics, i.e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability...

Full description

Bibliographic Details
Main Authors: Jakub Michaliszyn, Jan Otop, Piotr Witkowski
Format: Article
Language:English
Published: Open Publishing Association 2012-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1210.2481v1
_version_ 1798044936523743232
author Jakub Michaliszyn
Jan Otop
Piotr Witkowski
author_facet Jakub Michaliszyn
Jan Otop
Piotr Witkowski
author_sort Jakub Michaliszyn
collection DOAJ
description We study elementary modal logics, i.e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and for finite satisfiability [11, 12, 16, 17]. In this paper, we show that there is a reason why we must deal with both kinds of satisfiability separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable (global) satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.
first_indexed 2024-04-11T23:13:16Z
format Article
id doaj.art-8611eead28704e349331fbda45dd531e
institution Directory Open Access Journal
issn 2075-2180
language English
last_indexed 2024-04-11T23:13:16Z
publishDate 2012-10-01
publisher Open Publishing Association
record_format Article
series Electronic Proceedings in Theoretical Computer Science
spelling doaj.art-8611eead28704e349331fbda45dd531e2022-12-22T03:57:45ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-10-0196Proc. GandALF 201214115410.4204/EPTCS.96.11Satisfiability vs. Finite Satisfiability in Elementary Modal LogicsJakub MichaliszynJan OtopPiotr WitkowskiWe study elementary modal logics, i.e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and for finite satisfiability [11, 12, 16, 17]. In this paper, we show that there is a reason why we must deal with both kinds of satisfiability separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable (global) satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.http://arxiv.org/pdf/1210.2481v1
spellingShingle Jakub Michaliszyn
Jan Otop
Piotr Witkowski
Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
Electronic Proceedings in Theoretical Computer Science
title Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
title_full Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
title_fullStr Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
title_full_unstemmed Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
title_short Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
title_sort satisfiability vs finite satisfiability in elementary modal logics
url http://arxiv.org/pdf/1210.2481v1
work_keys_str_mv AT jakubmichaliszyn satisfiabilityvsfinitesatisfiabilityinelementarymodallogics
AT janotop satisfiabilityvsfinitesatisfiabilityinelementarymodallogics
AT piotrwitkowski satisfiabilityvsfinitesatisfiabilityinelementarymodallogics