×

Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T. (English) Zbl 1156.03321

Kaminski, Michael (ed.) et al., Computer science logic. 22nd international workshop, CSL 2008, 17th annual conference of the EACSL, Bertinoro, Italy, September 16–19, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-87530-7/pbk). Lecture Notes in Computer Science 5213, 308-322 (2008).
Summary: 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.
For the entire collection see [Zbl 1148.68004].

MSC:

03B44 Temporal logic
03B25 Decidability of theories and sets of sentences
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI