[Prev][Next][Index][Thread]
Book announcement
Book announcement:
THE CLAUSAL THEORY OF TYPES
D.A. Wolfram
University of Oxford
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 new and concise form of
logic programming that incorporates functional programming is
acheived.
The book begins by reviewing the fundamental Skolem-Herbrand-Goedel
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.
The book can be used for graduate courses in theorem proving, but will
be of interest to all working in declarative programming.
1. Logic Programming: A Case Study; 2. Simply Typed lambda-Calculus;
3. Higher-Order Logic; 4. Higher-Order Equational Unification;
5. Higher-Order Equational Logic Programming.
132 pages; ISBN 0 521 39358 0 hardback; GBP 24.95
Cambridge Tracts in Theoretical Computer Science, Volume 21, 1993
Cambridge University Press
The Edinburgh Building, Cambridge CB2 2RU, UK.
40 West 20th Street, New York, NY 10011-4211, USA. Toll-free 800-872-7423
10 Stamford Road, Oakleigh, VIC 3166, Australia.