The clausal theory of types

著者

• Wolfram, D. A

書誌事項

The clausal theory of types

D.A. Wolfram

（Cambridge tracts in theoretical computer science, 21）

Cambridge University Press, 1993

• : hardback
• : pbk

注記

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」 より

詳細情報

• NII書誌ID(NCID): BA19744459
• ISBN:
  • 0521395380
  • 9780521117906
• 出版国コード: uk
• タイトル言語コード: eng
• 本文言語コード: eng
• 出版地: Cambridge
• ページ数/冊数: viii, 124 p.
• 大きさ: 26 cm
• 分類:
  • DC20 : 005.131
• 件名:
  • LCSH : Logic programming
• 親書誌ID:
  • BA01121831