bokomslag The Clausal Theory of Types
Data & IT

The Clausal Theory of Types

D A Wolfram

Pocket

739:-

Funktionen begränsas av dina webbläsarinställningar (t.ex. privat läge).

Uppskattad leveranstid 5-10 arbetsdagar

Fri frakt för medlemmar vid köp för minst 249:-

Andra format:

  • 136 sidor
  • 2009
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-Gdel 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.
  • Författare: D A Wolfram
  • Format: Pocket/Paperback
  • ISBN: 9780521117906
  • Språk: Engelska
  • Antal sidor: 136
  • Utgivningsdatum: 2009-07-30
  • Förlag: Cambridge University Press