Temporal Logic

Temporal logic focus on logical statements that include a particular Logical time point or a particular Logical time range.

Much logic is atemporal, in that it is always true, and thus does not need a reference to time within the Logical Context that is needed to evaluate if it is true or not.

Review of article: https://dl.acm.org/doi/10.1016/0004-3702%2891%2990025-F

A non-reified temporal logic

Authors: 

• Fahiem Ivor Bacchus profile imageFahiem Bacchus
• Josh D. Tenenberg profile imageJosh Tenenberg
• Johannes A G M Koomen profile imageJohannes A. Koomen

Reviewer:Vladik Ya. Kreinovich

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 on 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.