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-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. 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.

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

Book Information
ISBN 9780521395380
Author D. A. Wolfram
Format Hardback
Page Count 134
Imprint Cambridge University Press
Publisher Cambridge University Press
Weight(grams) 406g
Dimensions(mm) 254mm * 177mm * 11mm