TY  - BOOK
AU  - Padawitz,Peter
TI  - Computing in Horn clause theories
T2  - EATCS monographs on theoretical computer science
SN  - 0387194274
U1  - 005.11 23
PY  - 1988///
CY  - Berlin
PB  - Springer-Verlag
KW  - Logic programming
KW  - Horn clauses
N1  - 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
N2  - 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
ER  -