Extending temporal logic programming with choice predicates non-determinism

Mehmet A. Orgun*, William W. Wadge

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

11 Citations (Scopus)


In temporal logic programming, a stream can be specified by a single-valued, time-varying predicate which, at any given moment in time, represents the corresponding element in the stream. However, due to inherent non-determinism in logic programming, time-varying predicates do not necessarily represent single-valued relations at any given moment in time. Choice predicates are also time-varying predicates, but, in principle, they act like a dataflow node with multiple input lines which non-deterministically selects one of its inputs as output. Thus they are guaranteed to be single-valued at all moments in time, and they can be regarded as representing 'non-deterministic' streams. Users do not define choice predicates, they are supplied automatically for all predicates defined in temporal logic programs. Inputs to choice predicates are supplied by the corresponding predicates. When the connection between choice predicates and the corresponding predicates is established, we obtain non-Horn temporal logic programs as a result. The model-theoretic semantics of such a program is developed in terms of 'minimal models'. However, the logical structure of the program dictates which minimal models are constructible from the program. We in particular discuss a characterization of constructible minimal models as limits of alternating chains of models obtained by applications of two new mappings NTP and CP. The paper also outlines a proof procedure for the temporal language Chronolog extended with choice predicates.

Original languageEnglish
Pages (from-to)877-903
Number of pages27
JournalJournal of Logic and Computation
Issue number6
Publication statusPublished - Dec 1994


  • Alternating chains
  • Logic programming
  • Minimal models
  • Non-determinism
  • Proof procedures
  • Temporal logic


Dive into the research topics of 'Extending temporal logic programming with choice predicates non-determinism'. Together they form a unique fingerprint.

Cite this