``Clausal Theory of Types'' from Cambridge Univ. Press

Date: Tue, 15 May 90 11:43:15 BST

                 Cambridge University Press
      Cambridge Tracts in Theoretical Computer Science

                     Forthcoming Title


                        D.A. Wolfram
           Oxford University Computing Laboratory
                 Programming Research Group

This book introduces  a  theoretical  basis  for  resolution
theorem  proving  with  a  lambda  calculus formulation of a
higher-order clausal logic with equality, called the Clausal
Theory  of  Types.   The  fundamental Skolem-Herbrand-Goedel
Theorem and resolution are  generalized to the  higher-order
setting.  Operationally,  this  requires the introduction of
higher-order   equational   unification,   which   builds-in
higher-order equational theories.

When restricted to higher-order Horn clauses,  a  foundation
for  an  expressive  logic  programming language is provided
which has the unique properties of being sound and  complete
with respect to Henkin-Andrews general models, and of treat-
ing functionally equivalent terms as  identical.   Canonical
general  model  theoretic  characterizations of provable and
finitely-failed formulas are  presented for  Clausal  Theory
of  Types  Horn  clauses,  which extrapolate the first-order

Contents: Introduction and Related Work; Logic  Programming:
A  Case  Study;  The Skolem-Herbrand-Goedel Theorem; Resolu-
tion; Least Model Semantics; Computational  Adequacy;  Nega-
tion;  Simply  Typed  Lambda  Calculus;  Conversions; Normal
Forms; Substitutions; Higher-Order  Logic;  General  Models;
The  Clausal  Theory  of  Types; lambda-Models; Higher-Order
Skolem-Herbrand-Goedel  Theorem;   Higher-Order   Equational
Unification;  Third-Order  Equational Matching; Higher-Order
Unification; Heuristics and Implementations;  Undecidability
Results; Decidability of Higher-Order Matching; Second-Order
Monadic  Unification;  First-Order  Equational  Unification;
Higher-Order   Equational  Logic  Programming;  Higher-Order
Equational Resolution; CTT as a Programming Language;  Least
CTT  Models;  Soundness  and  Completeness;  Declarative and
Operational Semantics; Bibliography.