Go to home page  |   Undecidability of RRA  |  Monodic fragments of predicate temporal logic

On modal logics between KxKxK and S5xS5xS5 (draft version)

Robin Hirsch, Ian Hodkinson, Agi Kurucz
J. Symbolic Logic 67 (2002) 221-234.
We prove that every 3-dimensional modal logic between K3 and S53 is undecidable. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic.  The proofs combine the modal logic technique of Jankov-Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the (undecidable) representation problem for finite relation algebras.

Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T

Ian Hodkinson, Angelo Montanari, and Guido Sciavicco
In: Proc. CSL 2008, M. Kaminski and S. Martini (Eds.), LNCS 5213, 2008, pp. 307-321.
Interval logics are an important area of computer science.  Although attention has been mainly focused on unary operators, an early work by Venema (1991) introduced an expressively complete interval logic language called CDT, based on binary operators, which has many potential applications and a strong theoretical interest.  Many very natural questions about CDT and its fragments, such as (non-)finite axiomatizability and (un-)decidability, are still open (as a matter of fact, only a few undecidability results, including the undecidability of CDT, are known).  In this paper, we answer most of these questions, showing that almost all fragments of CDT, containing at least one binary operator, are neither finitely axiomatizable with standard rules nor decidable.  A few cases remain open.