ONTIC

About this 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.

Themes & subjects

About the author

David A. McAllester

Professor David A. McAllester received his B.S., M.S., and Ph.D. degrees from the Massachusetts Institute of Technology in 1978, 1979, and 1987 respectively. After graduating, he taught at Cornell University for one year. In 1988 he moved to MIT. In 1995 he became a member of technical staff at AT&T Labs-Research, where he stayed until 2002. In 1997 he became a fellow of the American Association of Artificial Intelligence (AAAI). He is currently a professor at the Toyota Technological Institute at Chicago. McAllester's research interests include machine learning theory, programming language theory, automated reasoning, AI planning, and computational linguistics.