Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T

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.

• Type: Conference
• Year: 2008
• Where: CSL
• Authors: Ian Hodkinson, Angelo Montanari, Guido Sciavicco
• Keywords: Automated Reasoning, Binary Operator, CSL 2008, Interval Logic, Language Called Cdt