Foundations of linear-time logic programming

M. A. Orgun*

*Corresponding author for this work

Research output: Contribution to journalArticle

2 Citations (Scopus)

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.

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

Keywords

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

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

Cite this