Cover of: ONTIC | David A. McAllester

About the Book

ONTIC, the interactive system for verifying "natural" mathematical arguments that David McAllester describes in this book, represents a significant change of direction in the field of mechanical deduction, a key area in computer science and artificial intelligence. ONTIC is an interactive theorem prover based on novel forward chaining inference techniques. It is an important advance over such earlier systems for checking mathematical arguments as Automath, Nuprl, and the Boyer Moore system. The first half of the book provides a high-level description of the ONTIC system and compares it with these and other automated theorem proving and verification systems. The second half presents a complete formal specification of the inference mechanisms used. McAllester's is the only semi automated verification system based on classical Zermelo-Fraenkel set theory. It uses object oriented inference, a unique automated inference mechanism for a syntactic variant of first order predicate calculus. The book shows how the ONTIC system can be used to check such serious proofs as the proof of the Stone representation theorem without expanding them to excessive detail.

Edition Notes

Series Artificial intelligence

The Physical Object

Format Hardcover
Number of pages 174
Dimensions 9.2 x 6.2 x 0.8 inches
Weight 1 pounds

ID Numbers

Open Library OL10237356M
Internet Archive ONTICAKnow_00_McAl
ISBN 10 0262132354
ISBN 13 9780262132350

Borrow eBook

Prefer the physical book? Check nearby libraries with:

Buy this book

Amazon $4.50 (used)
Better World Books $$3.48 (used) (used)


Download catalog record: RDF / JSON / OPDS
June 13, 2018 Edited by LeadSongDog Edited without comment.
January 26, 2018 Edited by ImportBot import new book
April 13, 2010 Edited by Open Library Bot Linked existing covers to the edition.
December 15, 2009 Edited by WorkBot link works
April 30, 2008 Created by an anonymous user Inital record created, from an record.