Extending Temporal Logic Programming with

Choice Predicates Non-determinismy

MEHMET A. ORGUN WILLIAM W. WADGE

Department of Computing Department of Computer Science

Macquarie University University of Victoria

Sydney, NSW 2109, Australia Victoria, B.C. V8W 3P6, Canada

Abstract

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. Therefore they are guaranteed to be single-valued at all moments in time, and they can be regarded as representing on-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 chains of models obtained by alternating applications of two new mappings NTP and CP . The paper also outlines a proof procedure for the temporal language Chronolog extended with choice predicates.

1 Introduction

In logic programming languages, streams are usually represented by infinitary data structures such as infinite lists. Through streams, non-terminating dataflow computations can be modeled in concurrent logic programming languages such as Parlog [14]

yTo appear in Journal of Logic and Computation