The natural straightforward way to express properties that change in time is to add time as an argument to all the functions, propositions, and predicates. Those who formalize commonsense reasoning rarely do this, for two reasons. First, they formalize how people think, and when we draw conclusions about things that change we rarely mention time explicitly. Second, this knowledge is usually represented as a logic program, and if we add an extra argument to all the predicates we drastically increase the set of ground atoms (and thus the running time of the logic program). Therefore, special formalisms called reified logics are usually used. In these formalisms, propositions P (such as ( A , B )) are the same as when nothing changes in time. The difference is that we use auxiliary predicates like Holds ( P , t ) or True ( t 1 , t 2 , P ) to describe the truth of propositions that change over time.
In general, this approach works fine, but two problems remain. First, if we formalize complicated statements referring to different moments of time, the formalizations become clumsy (the authors’ example is “The President of 1962 died in 1963”). Second, we are not in first-order logic (FOL), so we cannot use developed FOL techniques for proof search. To resolve these problems, the authors propose using time as an additional predicate. Thus we are sure that our theories are complete (due to completeness theorems for FOL), and we can use known methods for proof search. The authors prove that reified logics can be translated into this new formalism, and therefore the knowledge expressed in reified form can easily be combined with the non-reified form.
