Brief: Seeks to formalize mathematical knowledge within CYC
Jump To: Parent Description

  • MKM is a recent branch of mathematics dealing with repositories of mathematical knowledge. The CYC system's ontology rather conspicuously lacks a detailed mathematical KB, seeing as CYC is derived from AM (Auto-Mathematician). Giving CYC the ability to prove theorem from mathematics will help with its reasoning abilities when trying to solve problems with automated theorem proving, especially program synthesis problems involving computability and complexity. It will also help with intelligent tutoring systems. The techniques developed for MKM will then be applied to other areas of study, such as computer science and artificial intelligence.