## Logic Programming: Operational Semantics and Proof Theory

**J H Andrews**
*Abstract:* Logic programming systems which use parallel
strategies for computing ``and'' and ``or'' are theoretically
elegant, but systems which use sequential strategies are far more
widely used and do not fit well into the traditional theory of
logic programming. This thesis presents operational and
proof-theoretic characterisations for systems having each of the
possible combinations of parallel or sequential ``and'' and
parallel or sequential ``or''.

The operational semantics are in the form of an abstract
machine. The four control strategies emerge as simple variants of
this machine with varying degrees of determinism; some of these
variants have equivalent, compositional operational semantics,
which are given.

The proof-theoretic characterisations consist of a single
central sequent calculus, LKE (similar to Gentzen's sequent
calculus for classical first order logic), and sets of axioms which
capture the success or failure of queries in the four control
strategies in a highly compositional, logical way. These
proof-theoretic characterisations can be seen as logical semantics
of the logic programming languages.

The proof systems can also be used in practice to prove more
general properties of logic programs, although it is shown that
they are unavoidably incomplete for this purpose. One aspect of
this incompleteness is that it is not possible to derive all valid
sequents having free variables; however, induction rules are given
which can help to prove many useful sequents of this kind.

**PhD Thesis - Price £8.00**

*LFCS report ECS-LFCS-91-142 (also published as
CST-75-91)*

Previous |

Index |

Next