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...
Main Authors: | , , |
---|---|
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 |