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 linear-time temporal logic with unbounded past and future. It is suitable for applications involving the notion of dynamic change such as modelling periodical changes, non-terminating 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 resolution-type proof procedure called TiSLD-resolution. TiSLD-resolution is based on the axioms and the rules of inference of the underlying temporal logic. It is shown that TiSLD-resolution 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 time-dependent and dynamic properties of certain problems in a natural and problem-oriented 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 linear-time 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 26-27, 1993, Universit?e Laval, Qu?ebec City, Canada.