**A PROOF PROCEDURE FOR TEMPORAL LOGIC PROGRAMMING**

**Manolis Gergatsoulis, Christos Nomikos**

In this paper, we propose a new resolution proof procedure
for the branching-time logic programming language Cactus.
The particular strength of the new proof procedure,
called {\em CSLD-resolution},
is that it can handle, in a more general way,
open-ended queries, i.e. goal clauses that include atoms which do
not refer to specific moments in time,
without the need of enumerating
all their canonical instances. We also prove
soundness, completeness and independence of the computation rule
for CSLD-resolution.
The new proof procedure overcomes the limitations of a family of proof
procedures for temporal logic programming languages, which were
based on the notions of canonical program and goal clauses.
Moreover, it applies directly to Chronolog programs
and it can be easily extended to apply to multi-dimensional logic programs
as well as to Chronolog(MC) programs.

**Keywords**: Temporal Logic Programming, Proof Procedures, Branching-Time,
Theorem Proving.