# 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)