**Calendar Logic**

*Hans Jürgen Ohlbach and Dov Gabbay*

**Abstract:**

A propositional temporal logic is introduced whose operators quantify
over intervals of a reference time line. The intervals are specified
symbolically, for example `* next week's weekend*'.
The specification language for the intervals
takes into account all the features of real calendar systems. A simple
statement which can be expressed in this language is for example:
`yesterday I worked for eight hours with one hour lunch break at
noon'. Calendar Logic can be translated into propositional logic.
Satisfiability is therefore decidable.
Since the translation is exponential,
a tableau decision procedure for checking decidability is presented
as an alternative.

**Download**

uncompressed files | dvi (145K) | PostScript (334K) | PDF (254K) | bib |

compressed files | dvi ( 54K) | PostScript (120K) | PDF (226K) |

**Calendar Logic**

*Hans Jürgen Ohlbach*

uncompressed files | dvi (494K) | PostScript (1.1M) | PDF (698K) | bib |

compressed files | dvi (168K) | PostScript (307K) | PDF (547K) |