The Clausal Theory of Types

Appeared in Volume 8/3, August 1993

Keywords: typing.

D.A. Wolfram
Univ. of Oxford
Email: David.Wolfram@prg.oxford.ac.uk

Logic Programming was based on first-order logic. Higher-order logics can also lead to theories of theorem proving. This book introduces just such a theory, based on a lambda-calculus formulation of a clausal logic with equality known as the Clausal Theory of Types. By restricting this logic to Horn clauses, a new and concise form of logic programming that incorporates functional programming is acheived.

The book begins by reviewing the fundamental Skolem-Herbrand-Goedel Theorem and resolution, which are then extrapolated to a higher-order setting; this requires introducing higher-order equational unification which builds-in higher-order equational theories and uses higher-order rewriting.

The logic programming language derived has the unique property of being sound and complete with respect to Henkin-Andrews general models, and consequently of treating equivalent terms as identical.

The book can be used for graduate courses in theorem proving, but will be of interest to all working in declarative programming.

1. Logic Programming: A Case Study
2. Simply Typed lambda-Calculus;
3. Higher-Order Logic
4. Higher-Order Equational Unification;
5. Higher-Order Equational Logic Programming.

132 pages; ISBN 0 521 39358 0 hardback; 24.95 pounds
Cambridge Tracts in Theoretical Computer Science, Vol. 21, 1993

Cambridge University Press
The Edinburgh Building
Cambridge CB2 2RU, UK

40 West 20th Street
New York, NY 10011-4211, USA
Toll-free tel: 800 872 7423