Chronolog(Z): Linear-time logic programming
Mehmet A. Orgun William W. Wadge Weichang Du
Department of Computing Department of Computer Science Department of Computer Science Macquarie University University of Victoria University of New Brunswick Sydney, NSW 2109, Australia Victoria, B.C. V8W 3P6, Canada Saint John, N.B., Canada
This paper introduces Chronolog(Z), a logic programming language based on a discrete linear-time temporal logic with unbounded past and future. Chronolog(Z) is suitable for applications involving the notion of dynamic change such as modeling nonterminating computations, the simulation of sequential circuits, and temporal databases. The execution of the programs of the language is based on a resolution-type proof procedure called TiSLD-resolution. A modular extension of Chronolog(Z) is proposed which can be used to model objects with internal memory.
Temporal logic has been successfully used as a formalism in concurrent program specification and verification, modeling temporal databases, and various forms of temporal reasoning. In temporal logic , the meanings of formulas vary depending on an implicit time parameter and elements from different moments in time can be combined through the use of temporal operators, not by explicit references to time. More recently, a number of logic programming languages based on diverse temporal logics have been proposed: Tempura  and Tokio  are based on interval logic; Templog  and Chronolog  are based on linear-time temporal logics and Temporal Prolog  is based on linear and branching time temporal logics.
In Tempura, programs are systematically transformed into a sequence of state descriptions over an interval that satisfies the original program . Templog , Temporal Prolog  and Chronolog  are extensions of logic programming in which temporal logic programs are executed to obtain answers by the use of resolution-type proof procedures. Tokio has a mixed execution mechanism .
There are also several attempts at developing semantics of temporal logic languages. Baudinet  showed that Templog's proof procedure is sound and
complete; and established the equivalence of the declarative and the operational semantics of Templog programs. Orgun and Wadge [13, 14] provided the semantics of Chronolog programs and outlined a complete proof procedure for the language. Gabbay  defined a resolution procedure for Temporal Prolog and proved its soundness. These results suggest that temporal logic programming is feasible.
This paper in particular introduces the temporal language Chronolog(Z), which is an extension of Chronolog , based on a linear-time temporal logic with unbounded past and future with the set Z of integers as the collection of moments in time. The temporal logic of Chronolog(Z) has an operator to look into the past as well as the operators first and next of Chronolog. The execution" of Chronolog(Z) programs is based on a resolution-type proof procedure called TiSLD-resolution. In , it is also shown that the declarative and the operational semantics of Chronolog(Z) programs coincide.
Consider the following program that defines the predicate f which is true of the t + 1th Fibonacci number for time t >= and no other.
first next f(1).
next next f(N) <- next f(X), f(Y), N is X+Y.
Read all clauses as assertions true at all moments in time. The first two clauses define the first two Fibonacci numbers as 1; and the last clause defines the current Fibonacci number as the sum of the previous two. For example, the answer to the given goal <- first next next f(X) is a (substitution) instance of the goal with X replaced by 2.
In the following, we first outline the temporal logic of Chronolog(Z). We then discuss several applications of the language, including modeling non-terminating computations and the simulation of sequential circuits. We also propose a modular extension of Chronolog(Z) for specifying objects with internal memory.