A computational logic handbook
This book provides the definitive documentation for one of the most well-known and highly regarded theorem-proving programs ever written. The program described is one of the more significant, enduring, and prize-awarded accomplishments in the fields of artificial intelligence, formal methods, and applied logic. The book provides an exact statement of the logic for which the program is a prover, a complete description of the user's commands, installation instructions, and much tutorial information, including references to thousands of pages of examples. Among the examples is a formally verified microprocessor and a formally verified compiler targeting that microprocessor. The second edition of A Computational Logic handbook provides all the information necessry for using the most recently releases version of Nqthm, the freely available"Boyer-Moore"theorem-proving program. The second edition includes a precise description of all recent changes to the logic in the past nine years, including many enhanced syntactic features and rules of inference, which were added to support work on large scale projects in formal methods. Thousands of pages of fascinating, exemplary, mathematically-checked input are described, examples that deal with very difficult questions in formal mehtods and mathematics. New material includes: Description of the new syntax, including COND, CASE, LET, LIST*, and backquote; describes some higher order inference procedures, including"constrained functions"and"functional instantiation"; documents more sophisticated control machinery for manipulating very large theories; introduces a secure proof-checking environment; describes thousands of pages of fascinating example input dealing with very difficult questions in formal methods and mathematics; provides a formal parserfor the syntax; compares the proof complexity of many interesting checked examples; includes much new tutorial help, especially for the many new features. A computational logic is a mathematical logic that is both oriented towards discussion of computation and mechanised so that proofs can be checked by computation. The computational logic discussed in the handbook is that developed by Boyer & Moore. The first edition, published in 1988, is an acknowledged classic in the field of formal methods and computational logic. However it no longer reflects existing technology. The second edition provides a complete overview of the Boyer/Moore theorem proving approach (Nqthm) and provides examples. It includes several significant new features that have been aded to the Nquthm system since 1988. The book is structured in thefollowing way: Part 1 discusses logic without regard for its mechanisation and answers the question what are the axioms and rules of inference? Part 2 discusses its mechanisation and answers the question how does one use the Boyer/Moore theorem prover to prove theorems?
15 pages matching APPEND A B in this book
Results 1-3 of 15
What people are saying - Write a review
A Primer for the Logic
Formalization Within the Logic
15 other sections not shown
A computational logic handbook
A computational logic handbook. Purchase this Book. Source, Academic Press Perspectives In Computing archive. Pages: 408. Year of Publication: 1988 ...
A Computational Logic Handbook: Second Edition
Robert S. Boyer and J Strother Moore, A Computational Logic Handbook, Second Edition, Academic Press, 1998, ISBN 0121229556. 518+xxv pages. ...
www.cs.utexas.edu/ ~boyer/ aclh2-blurb.html
Review: Robert S. Boyer, J. Strother Moore, A Computational Logic ...
Robert S. Boyer, J. Strother Moore, A Computational Logic Handbook. Full-text: Access via JSTOR (no additional login). Go to this article in JSTOR ...
projecteuclid.org/ handle/ euclid.jsl/ 1183743422
Interaction with the Boyer-Moore theorem prover: A tutorial study ...
Journal of Automated Reasoning. 16:181-222, 1996. 181. ( 1996. Kluwer Academic Publishers. Printed in the Netherlands. Interaction with the Boyer-Moore ...
www.springerlink.com/ index/ U3644488U01400P7.pdf
Mechanically verifying concurrent programs with the Boyer-Moore ...
IEEE. TRANSACTIONS ON SOFTWARE ENGINEERING. VOL 16. NO. 9, SEPTEMBER 1990. 100.5. Mechanically Verifying Concurrent Programs with. the Boyer-Moore Prover ...
ieeexplore.ieee.org/ iel1/ 32/ 2136/ 00058787.pdf
 rs Boyer and js Moore. (researchindex)
A Computational Logic Handbook. Academic Press, 1988.  A. Coglio.... Home/Search Context Related. View or download: sra.itc.it/tr/AM96.ps.gz ...
Robert S. Boyer - Wikipedia, the free encyclopedia
A Computational Logic Handbook, with J S. Moore. Second Edition. Academic Press, London, 1998. Automated Reasoning: Essays in Honor of Woody Bledsoe, ...
en.wikipedia.org/ wiki/ Robert_S._Boyer
JSTOR: A Formal HDL and its Use in the FM9001 Verification
The syntax, axioms, and rules of inference of the logic are given precisely in A computational logic handbook (Boyer & Moore 1988). ...
CLI Technical Reports September 6, 1994
This report contains the Common Lisp source code for the Boyer-Moore theorem prover, the program described in the book, A Computational Logic Handbook, ...
www.computationallogic.com/ reports/ abstracts.html
AARNEWS - December 1997
The second edition of the book A Computational Logic Handbook, by Robert S. Boyer and J Strother Moore, has recently been published by Academic Press (1997, ...
www.mcs.anl.gov/ AAR/ issuedec97/