ONTIC: A Knowledge Representation System for Mathematics
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.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Ontic in Brief
Comparison with Other Work
Ontic as a Cognitive Model
4 other sections not shown
Other editions - View all
3-conversion A-expression A-function A-type arbitrary Artificial Intelligence Automated Automated Theorem Proving axioms backward chaining Boolean circuit Boolean constraint propagation Boolean lattice bound variable Boyer-Moore color label congruence closure congruence combinator constraint propagation construct context defined definition denotes derived equals equation equivalence example exists EXISTS-SOME FAMILY-INTERSECTION finite focus objects focus set focused binding FORALL formula forward chaining free variable freevars graph structure higher-order ill-formed IN-CONTEXT individual induction inference mechanisms inference process inference rules instance IS-EVERY Knuth-Bendix procedure label propagation LAMBDA xT lattice LET-BE mapped mathematical member of F MEMBER-OF multiset natural deduction nodes NOTE-GOAL notion Ontic language Ontic proof Ontic system predicate proof expression quantifier-free quantifiers reification representation rewrite rules rules of obviousness semantic modulation set theory specifically subexpression subset SUBSET-OF subvariable symbol syntactically small term THE-SET-OF-ALL theorem proving tion topological space type expression type-generator unification variable of type variable XT verification system verify