peer reviewed

This paper addresses semantic and expressiveness issues for temporal logic programming and in particular for the TEMPLOG language proposed by Abadi and Manna. Two equivalent formulations of TEMPLOG's declarative semantics are given: in terms of a minimal Herbrand model and in terms of a least fixpoint. By relating these semantics to TEMPLOG's operational semantics, we prove the completeness of the resolution proof system underlying TEMPLOG's execution mechanism. To study TEMPLOG's expressiveness, we consider its propositional version. We show how propositional TEMPLOG programs can be translated into a temporal fixpoint calculus and prove that they can express essentially all regular properties of sequences.

A method for proving termination properties of Prolog programs including program with cuts. Programs are viewed as functions mapping goals into finite or infinite sequences of answer substitutions. Associated with each program is a system of functional equations, the least fixed point of which is the meaning of the program. Various termination or nontermination properties as well as partial correctness statements can then be proved by reasoning with the program equations and using fixpoint or structural induction. The method is amenable to automatic implementation.>