000			01544nam a22001937a 4500
005			20250717151238.0
008			250717b |||||||| |||| 00| 0 eng d
020			_a9780521117906 _qpbk
041			_aeng
082			_a005.115 _bWOL
100			_aD.a. Wolfram
245			_aThe Clausal Theory Of Types _cD.A Wolfram
260			_aUk25 _bCambridge University Press _c2009
300			_aVIII, 124 p. _c25 cm.
504			_aindex
520			_aLogic 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-Gödel 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.
650			_aProgramming Language
942			_cENGLISH
999			_c576100 _d576100