Dr. Hans Jürgen Ohlbach

Selected Publications in Calendar Logics

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

Abstract:
In this chapter we link temporal logic to real time calendar systems. Instead of the very general operators like `sometimes in the future' or `always in the future' we introduce relativized operators of the kind `sometimes next week' or `always in the office hours'. Calendar Logic is developed in three stages. We start with a system for specifying everyday temporal notions like `hours', `weeks', `weekend', `office-hour', `holiday' within a given calendar system. In this system one can check whether a given point in time lies within an interval specified by a time term, or whether a subsumption relation holds between two time terms. In the next stage these temporal notions are integrated into a propositional modal logic with two parameterized operators `sometimes within t' and `always within t' where t may be one of the previously defined temporal notions. An example for a statement in this logic is [2000,year]<June x_year>election. It expresses that some time in June in the year 2000 there is an election. [2000,year] denotes the time region corresponding to the year 2000. June x_year is a time term. It denotes a function that takes a year coordinate as argument and returns a month coordinate. Temporal expressions like these are not built-in, but they can be defined with some primitive constructors.

In the last stage, Calendar Logic will be combined with other (multi-) modal logics, for example modal logics of knowledge and belief. A simple statement in this logic is [1998,year][believe\_I] < x_year+1><June y_year> election. (In 1998 I believe that at some time in June the year after (i.e. 1999) there is an election.) A formula in a combination of Calendar Logic and an ALC-like Description Logic is <1996>(car & <sold>woman). It denotes the set of cars sold to women in the year 1996.

Download
uncompressed files dvi (494K) PostScript (1.1M) PDF (698K) bib
compressed files dvi (168K) PostScript (307K) PDF (547K)

Last Modified: Thursday, 06-Apr-2000 17:58:03 CEST