@book {IOPORT.00193479,
    author       = {Boyer, Robert S. and Moore, J. Strother},
    title        = {A computational logic handbook.},
    year         = {1988},
    isbn         = {0-12-122952-1},
    pages        = {xvi, 408 p.},
    publisher    = {Boston, MA etc.: Academic Press, Inc.},
    abstract     = {This book is a continuation of the same authors' previous book entitled ``A computational logic'' (1979; Zbl 0448.68020). The truly important changes to the theorem prover since 1979 are the integration of a linear arithmetic decision procedure and the addition of a rather primitive facility permitting the user to give hints to the theorem prover. The significant changes in the logic itself are the efficient use of functions in the logic as new proof procedures upon the establishment of their soundness and the permission of bounded quantification and partial recursive functions. These changes in the logic were described completely in their ``Metafunctions: proving them correct and using them efficiently as new proof procedures'' [in ``The correctness problem in computer science'' (1981; Zbl 0476.68009)] and ``The addition of bounded quantification and partial functions to a computational logic and its theorem prover'' [J. Autom. Reasoning 4, No.2, 117-172 (1988)]. However, as a whole, there have been comparatively minor changes to the logic and the theorem prover since the publication of the authors' former book, while the system has been applied to more and more difficult problems by more and more people. This book is intended as an updated thorough treatment of how to use the logic and the theorem prover.},
    reviewer     = {H.Nishimura},
    identifier   = {00193479},
}