| 000 | 00935camuu2200289 a 4500 | |
| 001 | 000045453828 | |
| 005 | 20080717105112 | |
| 008 | 931222s1993 enk b 001 0 eng d | |
| 010 | ▼a 93246461 | |
| 020 | ▼a 0521395380 (hardback) | |
| 020 | ▼a 9780521395380 | |
| 035 | ▼a (KERIS)REF000006693556 | |
| 040 | ▼a Uk ▼c Uk ▼d OCU ▼d DLC ▼d 211009 | |
| 042 | ▼a lccopycat | |
| 050 | 0 0 | ▼a QA76.63 ▼b .W64 1993 |
| 082 | 0 0 | ▼a 005.1/1 ▼2 20 |
| 082 | 0 4 | ▼a 005.115 ▼2 22 |
| 090 | ▼a 005.115 ▼b W861c | |
| 100 | 1 | ▼a Wolfram, D. A. |
| 245 | 1 4 | ▼a The clausal theory of types / ▼c D.A. Wolfram. |
| 260 | ▼a Cambridge ; ▼a New York : ▼b Cambridge University Press , ▼c 1993. | |
| 300 | ▼a viii, 124 p. ; ▼c 26 cm. | |
| 490 | 0 | ▼a Cambridge tracts in theoretical computer science ; ▼v 21 |
| 504 | ▼a Includes bibliographical references (p. 107-120) and index. | |
| 650 | 0 | ▼a Logic programming. |
| 945 | ▼a KINS |
소장정보
| No. | 소장처 | 청구기호 | 등록번호 | 도서상태 | 반납예정일 | 예약 | 서비스 |
|---|---|---|---|---|---|---|---|
| No. 1 | 소장처 과학도서관/Sci-Info(2층서고)/ | 청구기호 005.115 W861c | 등록번호 121173246 | 도서상태 대출가능 | 반납예정일 | 예약 | 서비스 |
컨텐츠정보
책소개
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-Godel 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.
In this book is presented the theoretical foundation of a higher-order logic programming language with equality, based on the clausal theory of types.
정보제공 :
목차
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.
정보제공 :