10
Views
2
CrossRef citations to date
0
Altmetric
Original Articles

Foundations of linear-time logic programming

Pages 199-219 | Received 23 Jan 1995, Published online: 19 Mar 2007
 

Abstract

This paper lays down foundations of logic programming based on a linear-time temporal logic with unbounded past and future. The resulting logic programming language is called Chronolog(ℒ). The language is suitable for applications involving the notion of dynamic change such as modeling periodical changes, historical databases and non-terminating computations. The declarative semantics of Chronolog(ℒ) programs is given in terms of temporal Herbrand models and the operational semantics in terms of a resolution-type proof procedure called TiSLD-resolution. It is shown that TiSLD-resolution is a sound and complete proof procedure. The equivalence of the declarative and the operational semantics of Chronolog(ℒ) programs is established. Extensions of Chronolog (ℒ) with extra temporal and modal operators such as “eventually” and “henceforth” are considered.

C.R. Categories:

Reprints and Corporate Permissions

Please note: Selecting permissions does not provide access to the full text of the article, please see our help page How do I view content?

To request a reprint or corporate permissions for this article, please click on the relevant link below:

Academic Permissions

Please note: Selecting permissions does not provide access to the full text of the article, please see our help page How do I view content?

Obtain permissions instantly via Rightslink by clicking on the button below:

If you are unable to obtain permissions via Rightslink, please complete and submit this Permissions form. For more information, please visit our Permissions help page.