The clausal theory of types

書誌事項

The clausal theory of types

D.A. Wolfram

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

関連文献: 1件中  1-1を表示

詳細情報

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