temporal logic

<logic> An extension of predicate calculus which includes notation for arguing about *when* statements are true. Time is discrete and extends indefinitely into the future. Three prefix operators, represented by a circle, square and diamond mean "is true at the next time instant", "is true from now on" and "is eventually true". x U y means x is true until y is true. x P y means x precedes y.

There are two types of temporal logic used: branching time and linear time. The basic propositional logic can not differentiate between the two, though.

(15 Jan 1997)