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.
Top page
Complete description
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.David A McAllester is an Assistant Professor of Computer Science at MIT. "ONTIC: A Knowledge Representation System for Mathematics" is included in the Artificial Intelligence series, edited by Patrick Henry Winston and Michael J. Brady.
Top page
General info
Publisher & Imprint:
MIT Press
City:
Cambridge, Mass.
Pages:
174
More info:
height 36 mm
width 58 mm
weight 454 gr
thickness 19 mm
“Knowledge has no limits” This site is owned by DEA Mediagroup SpA.
Tel. + 39 06 852121 Fax. + 39 06 8543228 Via Pietro Boccanelli 27 00138 Roma Italy
P.Iva 00901181008 Cod.Fiscale 00469620587
Send your comments or suggestions to:
customerservice@deastore.com
If you are experiencing problems using the system, please refer to the deastore Online Help Center or inform our Technical Support at:
helpdesk@deastore.com