Predicate Logic as a Computational Formalism

Keith L. Clark

The thesis treats the topic of the use of first order predicate logic as a languge for specifying, proving properties of, and programming computable relations and functions. The Horn clause subset with control annotations is the programming language and the program is invoked with a simple conjunctive query. The result of the query evaluation is a possibly open ended set of answer substitutions which bind all the variables of the query to terms that are computed data values. So logic programs compute relations. These data value terms may contain variables. When that is the case each answer sunstitution denotes a sub-relation of the computable relation.

For this programmimg subset of predicate logic the thesis gives: an operational semantics, describes how it can be efficiently implementated, introduces query evaluation control concepts and program and query annotations to express them, discusses algorithm design using Kowalski's logic + control concept, gives a model theory and fixed point semantics for the relation denoted by a query to a program, proves a strong equivalence of the fixed point and model theory semantics and operational semantics, shows that program verification is the proving of various theorems using a theory which is a first order consistent extension of the program, shows that logic program transformation and program synthesis are both the systematic deriving of Horn clause theorems from a first order theory of the relations to be computed.

A PDF file of the scanned thesis, 2 pages per A4 page

Click here (16.8MB)