Decidability
Go to home page | Undecidability of RRA
| Monodic fragments of
predicate temporal logic
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.
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.