Extending temporal logic programming with choice predicates non-determinism

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 NT_P and C_P. The paper also outlines a proof procedure for the temporal language Chronolog extended with choice predicates.