ONTIC: A Knowledge Representation System for Mathematics

Item

Title
en_US ONTIC: A Knowledge Representation System for Mathematics
Creator
en_US McAllester, David Allen
Date
2004-10-20T20:10:43Z
Date Available
2004-10-20T20:10:43Z
Date Issued
en_US 1987-07-01
Identifier
en_US AITR-979
Abstract
en_US Ontic is an interactive system for developing and verifying mathematics. Ontic's verification mechanism is capable of automatically finding and applying information from a library containing hundreds of mathematical facts. Starting with only the axioms of Zermelo-Fraenkel set theory, the Ontic system has been used to build a data base of definitions and lemmas leading to a proof of the Stone representation theorem for Boolean lattices. The Ontic system has been used to explore issues in knowledge representation, automated deduction, and the automatic use of large data bases.
Extent
44303384 bytes
35932682 bytes
Format
application/postscript
application/pdf
Language
en_US
Relation
en_US AITR-979