
Chronolog admits a complete proof procedurey
MEHMET A. ORGUN
Department of Computing, Macquarie University
Sydney, NSW 2109, Australia
and
WILLIAM W. WADGE
Department of Computer Science, University of Victoria
Victoria, B.C. V8W 3P6, Canada
Abstract
Chronolog(Z) is a logic programming language based on a lineartime temporal logic with unbounded past and future. It is suitable for applications involving the notion of dynamic change such as modelling periodical changes, nonterminating computations and temporal databases. The declarative semantics of Chronolog(Z) programs are given in terms of temporal Herbrand models and the operational semantics in terms of a resolutiontype proof procedure called TiSLDresolution. TiSLDresolution is based on the axioms and the rules of inference of the underlying temporal logic. It is shown that TiSLDresolution is sound and complete. The equivalence of the declarative and the operational semantics of Chronolog(Z) programs is also established.
AMS Subject Classification: 68N17 (Logic Programming).
1 Introduction
Temporal logic has been widely used as a formalism in concurrent program specification and verification [24], modelling temporal databases [25] and various forms of temporal reasoning [33]. In temporal logic [31], 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. Therefore temporal logic can model timedependent and dynamic properties of certain problems in a natural and problemoriented way. More recently, several researchers have suggested that temporal logic can be directly used as a programming language in applications involving the notion of dynamic change. A number of logic programming languages based on diverse temporal logics have been proposed: Tempura [27] and Tokio [3] are based on interval logic; Templog [2] and Chronolog [35] are based on lineartime temporal logic and Temporal Prolog [15] is based on linear and branching time temporal logics.
yTo be presented at ISLIP'93: The Sixth International Symposium on Lucid and Intensional Programming, April 2627, 1993, Universit?e Laval, Qu?ebec City, Canada.