|
Abstract : |
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., |
