Representation of Mathematical Knowledge in National Knowledge Infrastructure

The representation of mathematical knowledge is an important aspect of knowledge representation. It is the foundation for knowledge-based automated theorem proving, mathematical knowledge retrieval and intelligent tutoring systems, etc. According to the problems that are encountered in designing the mathematical knowledge representation language in NKI (national knowledge infrastructure) and after the discussion of ontological assumptions for mathematical objects, two kinds of formalisms for the representation of mathematical knowledge are provided. One is a description logic in which the range of an attribute can be a formula in some logical language; and another is a first order logic in which an ontology represented by the description logic is a part of the logical language. In the former representation, if no restrictions are imposed on formulas, then there is no algorithm to realize the reasoning in the resulted knowledge base; in the latter representation, the reasoning in the ontology represented by the description logic is decidable, while in general, for mathematical knowledge described by the first order logic which contains the ontology represented by the description logic, there is no algorithm to realize its reasoning. Hence, in the representation of mathematical knowledge, it is necessary to distinguish conceptual knowledge (knowledge in an ontology) and non-conceptual knowledge (knowledge represented by a language containing the ontology). Frames and description logics can represent and reason effectively about conceptual knowledge, but the addition of non-conceptual knowledge to frames or knowledge bases may make the reasoning in the resulted knowledge bases not decidable and there is even no algorithm to reason about the knowledge bases. Therefore, it is suggested that in representing mathematical knowledge, frames or description logics are used todescribe conceptual knowledge, and the logical languages containing the knowledge base represented by the frames or description logics are used to represent non-conceptual knowledge.