The Clausal Theory of Types

In this book is presented the theoretical foundation of a higher-order logic programming language with equality, based on the clausal theory of types.

D. A. Wolfram (Author)

9780521117906, Cambridge University Press

Paperback, published 30 July 2009

136 pages
24.4 x 17 x 0.7 cm, 0.23 kg

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 concise form of logic programming that incorporates functional programming is achieved. The book begins by reviewing the fundamental Skolem-Herbrand-Gödel 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. First published in 1993, the book can be used for graduate courses in theorem-proving, but will be of interest to all working in declarative programming.

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.

Subject Areas: Mathematical theory of computation [UYA]