The clausal theory of types
著者
書誌事項
The clausal theory of types
（Cambridge tracts in theoretical computer science, 21）
Cambridge University Press, 1993
- : hardback
- : pbk
大学図書館所蔵 全35件
注記
Includes bibliographical references (p. 107-120) and index
内容説明・目次
内容説明
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.
目次
- 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.
「Nielsen BookData」 より