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.