MKM

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 (AutoMathematician).
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.