Formal proofs of termination properties of Prolog programs with cut are presented which make use of an algebraic process semantics of Prolog. The algebraic semantics is written in Milner's CCS. This semantics treats Prolog program components as processes which generate streams of answer substitutions. Such characterisation of logic program computation is ideal for termination proofs because phenomena such as termination, infinite answer generation, and looping are easily modelled as streams. In addition, simple inductive proofs over streams or the structure of argument terms are readily supported. This paper suggests that the process algebra approach is a promising formalism for the semantics of different computational paradigms, since sequential as well as concurrent logic program execution is axiomatisable within it.
|Publisher||University of Edinburgh, Department of Artificial Intelligence|
|Publication status||Published - 1990|