ONTIC: A Knowledge Representation System for Mathematics

Abstract

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. Keywords: Cognitive models; Inference; Compilers; Programming languages; Stone representation theorem; Automated reasoning.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1987
Accession Number
ADA190553

Entities

People

  • David A. Mcallester

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Artificial Intelligence Computing
  • Boolean Algebra
  • Cognition
  • Computer Languages
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Formal Languages
  • Lisp Programming Language
  • Number Theory
  • Object Oriented Programming
  • Operating Systems
  • Programming Languages
  • Psychology
  • Set Theory

Fields of Study

  • Education

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • AI & ML
  • AI & ML - Information Retrieval