Foundations of linear-time logic programming

M. A. Orgun*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)199-219
Number of pages21
JournalInternational Journal of Computer Mathematics
Issue number3-4
Publication statusPublished - 1995


  • Declarative and Operational Semantics
  • Linear-Time Temporal Logic
  • Logic Programming
  • Properties of Temporal Operators
  • Temporal Resolution


Dive into the research topics of 'Foundations of linear-time logic programming'. Together they form a unique fingerprint.

Cite this