FOUNDATIONS OF LINEAR-TIME LOGIC PROGRAMMING

This paper lays down foundations of logic programming based on a linea r-time temporal logic with unbounded past and future. The resulting lo gic programming language is called Chronolog(L). The language is suita ble for applications involving the notion of dynamic change such as mo deling periodical changes, historical databases and non-terminating co mputations. The declarative semantics of Chronolog(L) programs is give n in terms of temporal Herbrand models and the operational semantics i n terms of a resolution-type proof procedure called TiSLD-resolution. It is shown that TiSLD-resolution is a sound and complete proof proced ure. The equivalence of the declarative and the operational semantics of Chronolog(L) programs is established. Extensions of Chronolog(L) wi th extra temporal and modal operators such as ''eventually'' and ''hen ceforth'' are considered.