Proof Procedures for Branching-Time Logic Programs

M. Gergatsoulis, P. Rondogiannis, T. Panayiotopoulos

Abstract
Traditional implementation techniques for temporal logic programming languages are based on the notion of canonical temporal atoms/clauses. Although such an approach is satisfactory for proving goals that refer to specific moments in time, it usually leads to non-terminating computations when considering open-ended goals. In this paper, we propose a new generalized proof procedure for implementing branching time logic programming languages. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle in a more general way open-ended queries, without the need of enumerating all their canonical instances.
Keywords: Temporal Logic Programming, Branching Time, Proof Procedures.