The Clausal Theory of Types

by D. A. Wolfram

Overview

This book presents the theoretical foundation of a higher-order logic programming language with equality, based on the clausal theory of types. A long-sought goal of logic programming, the clausal theory of types is a logic programming language that allows functional computation as a primitive operation while having rigorous, sound, and complete declarative and operational semantics. The language is very powerful, supporting higher-order equational deduction and functional computation. Its higher order syntax makes it concise and expressive, abstract data types can be expressed in it, and searching for multiple solutions is a basic operation. The author proves a number of important and surprising results: a Skolem-Herbrand-Gödel theorem for higher-order logic; a Higher-Order Resolution Theorem, which includes as special cases some previously unproven conjectures about equational matching and higher-order matching.

Product Details

ISBN-13:	9780521117906
Publisher:	Cambridge University Press
Publication date:	07/30/2009
Series:	Cambridge Tracts in Theoretical Computer Science , #21
Pages:	136
Product dimensions:	6.60(w) x 9.50(h) x 0.40(d)

Table of Contents

1. Introduction; 2. Logic programming: a case study; 3. Simply typed l-calculus; 4. Higher-order logic; 5. Higher-order equational unification; 6. Higher-order equational logic programming.

Editorial Reviews

This book has the merit of being very concise and yet rather comprehensive since it covers a broad range of issues related to higher-order logic and its application to automated theorem proving and logic programming. Its reading is recommended to any researcher in higher-order extensions of logic programming or in automated theorem proving.

Journal of Logic and Computation

The first major result of the book is a form of the "Skolem-Herbrand-Gödel'' theorem for the clausal theory of types. This is enough for the theory to be usable in principle as a programming language. To make it usable in practice, however, some form of unification is required, rather than an exhaustive search, and this leads to a discussion of the current state of knowledge in the field of higher-order unification.

Mathematical Reviews

Higher order analogues of the Skolem-Herbrand-Gödel theorem and resolution principle are proved and the equational unification of CTT terms with built-in equational theories is discussed in the book.

The author first proves the completeness of a procedure for equational unification of CTT terms and shows that the problem is undecidable. He moves on to higher-order matching. Thus this chapter also constitutes an excellent survey on this subject.

The bibliography, containing 204 reference items, is quite comprehensive and ought to be of great value to researchers in the area. The production of the book is excellent.

Computer Journal