[Prev][Next][Index][Thread]
``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
THE CLAUSAL THEORY OF TYPES
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
treatments.
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.