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.