The quest for programming languages which are more readable and expressive has led to many developments in programming languages, one of which is the logic programming paradigm. In theory, logic programming languages are more readable and expressive because they borrow some of the expressive power of the language of mathematical logic – a language which was developed specifically in order to model some of the deductive processes of the human mind.

This theoretical goal has been achieved to only a limited extent in practice, because the implementations of logic programming languages differ from the ideal theoretical model in many ways. One of the most basic and profound of the differences is that the theory concerns languages which can be implemented completely only by parallel (breadth-first) interpreters, while most practical implementations use incomplete, sequential (depthfirst) strategies.

This incompleteness in itself would not necessarily be a problem; but unfortunately, the exact set of terminating sequential logic programs is hard to characterise in a logical way. Sequentiality also affects reasoning about programs, disrupting the hope that the identification of program with logical formula would make this straightforward. These problems tend to weaken claims that practical and truly logical programming is possible.

This thesis is intended as a step towards mending this rift between theory and practice, between parallel and sequential systems. In the thesis, I present a homogeneous operational characterisation of the parallel and sequential versions of a basic logic programming language; I then use proof systems to characterise, in a logical manner, the sets of queries which terminate in the various parallel, sequential, and mixed control disciplines.