Computing in Horn clause theories / Peter Padawitz.
Material type:
- 0387194274
- 005.11 23 P123
Item type | Current library | Call number | Status | Date due | Barcode | Item holds | |
---|---|---|---|---|---|---|---|
Books | ISI Library, Kolkata | 511.3 P123 (Browse shelf(Opens below)) | Available | C26373 |
Includes indexes.
Bibliography: p. [307]-316.
1. Introduction--
2. Basic notions--
3. Sample specifications--
4. Models and theories--
5. Resolution and paramodulation--
6. The relevance of constructors--
7. Reduction--
8. Narrowing--
9. Church-Rosser criteria--
References--
Indexes.
This book presents a unifying approach to semantical concepts and deductive methods used in recursive, equational and logic programming, data type specification and automated theorem-proving. The common background is Horn logic with equality. Although this logic does not cover the full first-order logic, it supplies us with a language that allows "natural" problem specifications, offers several semantical views (functional, relational, inductive, behavioural, etc.) and puts at our disposal a number of more or less special-purpose deductive methods, which can be used as rapid prototyping tools.
There are no comments on this title.