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