Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Powiadomienia systemowe

Sesja wygasła!
Sesja wygasła!

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Satisfiability versus Finite Satisfiability in Elementary Modal Logics

Michaliszyn J., Otop J., Witkowski P.

Fundamenta Informaticae

2018

Vol. 163, nr 2

165--188

We study variants of the satisfiability problem of elementary modal logics, i.e., modal logic considered over first-order definable classes of frames. The standard semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. A number of decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and finite satisfiability. In this paper we justify that the results for both kinds of the satisfiability problem must be shown separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable general satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal first-order formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.

The Undecidability of the Logic of Subintervals

Marcinkowski J., Michaliszyn J.

Fundamenta Informaticae

2014

Vol. 131, nr 2

217--240

The Halpern–Shoham logic is a modal logic of time intervals. Some effort has been put in last ten years to classify fragments of this beautiful logic with respect to decidability of its satisfiability problem. We complete this classification by showing — what we believe is quite an unexpected result—that the logic of subintervals, the fragment of the Halpern–Shoham logic where only the operator “during”, or D, is allowed, is undecidable over discrete structures. This is surprising as this, apparently very simple, logic is decidable over dense orders and its reflexive variant is known to be decidable over discrete structures. Our result subsumes a lot of previous undecidability results of fragments that include D.