מיכאל קודיש

This paper presents a declarative semantics which exhibits the termination properties of a logic program. The semantics associates a program with its binary unfoldings — a possibly infinite set of binary clauses. Termination of a program P and goal G is indicated by the absence of an infinite chain in the binary unfoldings of P starting with G. The main contribution is a formal semantic basis for the termination analysis of logic programs which facilitates both design and implementation. As an implementation vehicle we propose a simple meta-interpreter for binary unfoldings and the use of an abstract domain based on symbolic norm constraints. Many of the recently proposed termination analyses for logic programs can be expressed concisely within our approach. To demonstrate our approach we have reformulated the analysis originally described in [13]. The implementation uses a standard library for linear equations over the recels. The combination of binary unfoldings and a constraint solver is shown to significantly simplify the design of the analysis.