A non-reified temporal logic

摘要

A temporal logic is presented for reasoning about propositions whose truth values might change as a function of time. The temporal propositions consist of formulae in a sorted first-order logic, with each atomic predicate taking some set of temporal arguments as well as a set of non-temporal arguments. The temporal arguments serve to specify the predicate's dependence on time. By partitioning the terms of the language into two sorts, temporal and non-temporal, time is given a special syntactic and semantic status without having to resort to reification. The benefits of this logic are that it has a clear semantics and a well-studied proof theory. Unlike the first-order logic presented by Shoham, propositions can be expressed and interpreted with respect to any number of temporal arguments, not just with respect to a pair of time points (an interval). We demonstrate the advantages of this flexibility. In addition, nothing is lost by this added flexibility and more standard and usable syntax. To prove this assertion we show that the logic completely subsumes Shoham's temporal logic [19].