An algebraic semantics of prolog program termination

Brian J Ross, Alan Smaill

Research output: Book/ReportBook


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.
Original languageEnglish
PublisherUniversity of Edinburgh, Department of Artificial Intelligence
Publication statusPublished - 1990

Fingerprint Dive into the research topics of 'An algebraic semantics of prolog program termination'. Together they form a unique fingerprint.

Cite this