+612 9045 4394
The Clausal Theory of Types : Cambridge Tracts in Theoretical Computer Science - D. A. Wolfram

The Clausal Theory of Types

Cambridge Tracts in Theoretical Computer Science


Published: 25th June 1993
Ships: 7 to 10 business days
7 to 10 business days
or 4 easy payments of $41.34 with Learn more

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 achieved. The book begins by reviewing the fundamental Skolem-Herbrand-Godel 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.

Logic programming: a case study
Simply typed l-calculus
Higher-order logic
Higher-order equational unification
Higher-order equational logic programming
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9780521395380
ISBN-10: 0521395380
Series: Cambridge Tracts in Theoretical Computer Science
Audience: Professional
Format: Hardcover
Language: English
Number Of Pages: 134
Published: 25th June 1993
Publisher: Cambridge University Press
Country of Publication: GB
Dimensions (cm): 26.04 x 18.42  x 1.27
Weight (kg): 0.41