Auto-construction for Knowledge Inheritance Hierarchy of Concepts within NKIMath

INTRODUCTION

Mathematical knowledge representation and acquisition are two major tasks in many mathematical applications, including knowledge-based automated theorem proving, integration of different mathematical software systems, mathematical semantic Web and high-level mathematical instruction (Asperti et al., 2001a, b; Zeng et al., 2004a, b). Recently, with the development and application of Web technology, mathematical markup language for the content and the context of mathematics toward Web, such as MathML (David et al., 2003), Open Math (Abbott et al., 1996) and OMDoc (Michael, 2001), has been received more attention and a lot of projects about mathematical domain knowledge base has been started including Mbase (Michael and Franke, 2001; Franke and Kohlhase, 2000), HELM (Asperti et al., 2001a; HELM), NOWGLI (Asperti and Wegner, 2002), etc.

In 1999, a long-term research project (called the National Knowledge Infrastructure, or NKI) was initiated in China to develop shareable knowledge bases of different domains and relevant underlying systems. Currently, the NKI contains knowledge from 21 domains, e.g., medicine, biology, history, geography, mathematics, music, ethnology and archaeology (Cao et al., 2002, 2004; Cao, 2001; Gu and Cao, 2001 ) and owns more than 350,000 concepts and 2,000,000 domain assertions. The knowledge of NKI is acquired from encyclopedia, dictionaries, handbooks, textbooks and so on, by semi-automatic and automated knowledge acquisition. NKI has two main purposes, one of which is to provide society-oriented knowledge services by Web, telephone, Email and another of which is to provide KAPI (knowledge application programming interface) for computer systems including language system, digital library, machine translation and so on.

NKIMath is the mathematical knowledge component of NKI (Cao et al., 2006; Zeng et al., 2003; Zeng et al., 2004a, 2006; Zeng, 2005), which is important for building the whole NKI project, not only because mathematics is a useful subject, but also mathematics is the foundation of lots of subjects, such as physics, mechanics and so on. According to the problems that are encountered in designing the mathematical knowledge representation language in NKI and after the discussion of ontological assumptions for mathematical objects, two kinds of formalisms for the representation of mathematical knowledge are provided in Cao et al. (2006). 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 predicate logic in which an ontology represented by the description logic is a part of the logical language Cao et al. (2006). The knowledge of NKIMath is acquired from mathematical encyclopedia, mathematical dictionaries, mathematical textbooks and s o on (Zeng et al., 2003). Knowledge engineers acquire knowledge from the knowledge sources and store them into the knowledge base (Zeng et al., 2004a). In order to manage the knowledge acquired within NKIMath and help the knowledge engineers acquire knowledge, a knowledge management platform, NKIMathE, has been designed and developed (Zeng et al., 2006).

To represent and acquire the knowledge of mathematics; especially mathematical concepts, the construction of the knowledge inheritance hierarchy between mathematical concepts, are important to realize knowledge inheritance between concepts. However, it is not easy to directly build the relations between concepts during knowledge acquisition since there are too many concepts. This study introduces the knowledge inheritance mechanism and the construction of knowledge inheritance hierarchy between concepts. Within NKIMath, a concept is represented by a knowledge frame, in which the formal definition of the concept is given by a logical formula in first-order logic (Cao et al., 2006). By the type of each concept, the concepts are divided into a set of concept categories. Within a concept category, the relations between concepts are defined. When the knowledge acquisition completed, the knowledge relations between concepts are auto-generated by reasoning, which include concept equivalence, concept subsumption, concept overlapping, concept exclusion and concept weak-correlation. With these relations, a three-level knowledge inheritance hierarchy of mathematical concepts can be constructed from the knowledge base, with which the knowledge can be inherited from one concept to another. Finally, an auto-construction algorithm is given to obtain the knowledge inheritance hierarchy between concepts from the knowledge base.

KNOWLEDGE REPRESENTATION FOR MATHEMATICS CONCEPT WITHIN NKIMATH

First, we present an example, the knowledge frame of the concept Monoid in NKIMath is shown in Fig. 1. Within the knowledge frame of Monoid, the knowledge is organized as four different components, which are:

Fig. 1:	The knowledge frame of concept Moniod

In NKIMath, the knowledge for each concept is represented by a frame embedded with a formula in first-order predicate logic and each frame is composed by a set of slots, where slots are either attributes or relations. The main attributes and relations of the knowledge frames for mathematical concepts include.

Name is an attribute presenting the name for each concept, which is distinguished from other concepts and can be referenced to. In different languages, different words are used to express one same concept. For example, Group in English, Gruppe in German are one same concept. A facet attribute LN specifies which language is used to express the name of the concept. Conforming to the XML recommendation, we use the ISO 639 two-letter country codes (EN for English, FR for French and CN for Chinese. . .) as the LN specification. This standard is also conformed to OMDoc (Michael, 2001).

Parameter is a special attribute to indicate the component of a concept and the methods to use the concept, which is a list of variables with Type facet to specify the type of each variable. For example, Monoid has two parameters, one of which is G with the type of Set (σ) and another is op with type σxσ→σ. It means that G and op are two components of Monoid and G and op are also two variables for predicate Monoid (G,op), which is used to determine whether a set and an operation compose a Monoid or not.

Context is an attribute to indicate a branch subject of mathematics, the main purpose of which is convenient for knowledge management. In the NKIMath knowledge management environment (Zeng et al., 2006) all the concepts with same Context value will be organized into one same subject. For example, Group, Abelian-Group all have the same Context value Group Theory, thus they belong to the same branch.

IFD (Informal Definition) and FD (Formal Definition) are two attributes to present the definitions of one same concept informally and formally towards different purposes.

IFD presents the user-oriented informal definition of the mathematical concept in natural language, which is used for knowledge querying, knowledge regeneration and knowledge instruction. It corresponds to the CMP element of OMDoc (Michael, 2001).

FD presents the machine-oriented formal definition with a logical formula in first-order logic (Cao et al., 2006), which is used for knowledge reasoning and theorem proving. FD is one of the most important attributes for mathematical concepts, which presents the formal intension for each concept and it is the basis of mathematical knowledge formalization. FD corresponds to the FMP element of OMDoc (Michael, 2001).

Pattern is an attribute to present the knowledge translation pattern, which serves for auto-generation of multi-lingual mathematical knowledge base to satisfy knowledge requirements of users with different language backgrounds. The Pattern attribute is one of the innovations for the mathematical concept knowledge representation in NKIMath. By now, we have presented the translation patterns in three kinds of languages including Chinese, English and German and realized to translate NKIMath into English and German automatically (Zeng et al., 2006).

Relations IS-A, SUBCATEGORY_OF and INSTANCE_OF give the relations between concepts. During the process of knowledge acquisition, these relations are not presented, which are auto-generated by the reasoning between FDs when knowledge acquisition completed.

Within the knowledge frame of a concept, there are other optional attributes, for example, [PROPOSER] gives the person(s) who first proposed the concept, [TIME_OF_PROPOSAL] gives the time of the first proposal about the concept and [PUBLICATION_ OF_PROPOSAL] indicates the source(s) where the concept was first published. All these attributes present some historical knowledge about the concept for educational purpose. Attributes PERIOD, INVERSE_ FUNCTION, IMAGE, DOMAIN and FIELD etc. are optional and are generally used to specify a mathematical function.

More details about the knowledge representation for mathematical concepts within NKIMath can be seen in Cao et al. (2006). In the following discussions of this paper, the Knowledge Base (KB) is a set of knowledge frames of mathematical concepts and it is assumed that KB is complete and correct. Knowledge errors and abnormities verification and checking methods for NKIMath can be seen in Zeng (2005).

CONCEPT CATEGORY AND CONCEPT RELATION

Here, the type of a mathematical concept is defined first, which is used to divided concepts into categories. Within a concept category, the relations between concepts will be defined, which include concept equivalence, concept subsumption, concept overlapping, concept exclusion and concept weak-correlation.

Concept category
Definition 1: The type of a mathematical concept C is type (C) = {σ| there is an object (instance) o ε E(C) such that the type of o is σ} where E(C) is the set of all the instances of concept C.

The type describes the composition of a mathematical concept. For example, the type of concept Group is Type(Group) = {(Set(σ), σxσ→σ)|σε MTSet}, where, MTSet is the set of all types. It indicates that every group is composed of a given set with type Set(σ) and a binary operation σxσ→σ on the set.

Let ConceptSet be the set of mathematical concepts. According to the types of mathematical concepts, an equivalence relation between concepts can be defined, thus ConceptSet can be divided into a set of equivalence classes. Every concept equivalence class is defined as a concept category.

Definition 2 ∀C₁, C₂ε ConceptSet, C₁ and C₂ satisfy type equivalence relation iff Type(C₁) = Type(C₂), denoted as

Proposition 1: The relation over ConceptSet is an equivalence relation.

Proof: It is easy to show that satisfies reflexivity, symmetry and transitivity, so is an equivalence relation.

Definition 3: The concept set ConceptSet can be divided into a set of equivalence classes according to each of which is named as a concept category.

Let be the set of all the concept categories and let be a concept category. With Definition 2, for any concept C₁, C₂ ε CAT, C₁ and C₂ satisfy Type(C₁) = Type(C₂). TypeLabel(C) is used to label the types of all the concepts in CAT, where C is any concept of CAT.

Based on the usual formalization of algebraic structures in type theory, the types of structures such as Group and Set (i.e., Type(Group) and Type(Set) in our notations) are Σ-types (Luo, 1999, 2008), with the former having the latter as a substructure. We can define a coercion carrier from groups to sets which extracts the type corresponding to the carrier set of a group. For example, G is a Group on set S and the carrier can be defined as Type(carrier(G)) = Type(S), thus all the properties satisfied on S are also satisfied on carrier(G). This kind of relation, such as there is a coercive function from Type(Group) to Type(Set), is defined as coercive subtyping.

Next, we define the inheritance relation between concept categories based on coercive subtyping.

Definition 4: Let be two concept categories. CAT₂ is a subcategory of CAT₁, or CAT₁ is a supercategory of CAT₂, if there is a coercive function from TypeLabel(CAT₁) to TypeLabel(CAT₂). Also, it is said that CAT₂ inherits from CAT₁, denoted as CAT₂ �< CAT₁.

If CAT₂ �< CAT₁ and TypeLbel(CAT₁) ≠TypeLabel (CAT₂), CAT₂ is a proper subcategory of CAT₁ and denoted as CAT₂ �< CAT₁.

With the properties of coercive subtyping, relation �< satisfies reflexivity and transitivity and relation �� satisfies non-reflexivity, non-symmetry and transitivity. Certainly, there are other relations between concept categories according to type theory (Luo, 1999, 2008). In this study, we only pay more attention to the inheritance relation between concepts, so other relations are not discussed here.

Relations between mathematical concepts: Within a concept category, all the concepts have same types, i.e., they have similar compositions. Between these concepts, five kinds of relations can be defined based on concept intensions (or FD knowledge), which are respectively concept equivalence, concept subsumption, concept overlapping, concept exclusion and concept weak-correlation.

Concept equivalence
Definition 5: Let be a concept category. ∀C₁, C₂ ε CAT, C₁ and C₂ satisfy the relation of concept equivalence (denoted as C₁ ≡ C₂), if KB, FD(C₁)||FD(C₂) and KB, FD(C₂)||FD(C₁).

In mathematics, different concepts can be used to express one same class of instances. Though the names of these concepts are different, their extensions are equal to each other and their intensions are equal in logic. For example, Abelian-group and commutative-group, complemented distributive lattice and distributive complemented lattice, triangle with equal edges and triangle with equal angles, satisfy the relation of concept equivalence, respectively.

Concept subsumption
Definition 6: Let be a concept category. ∀C₁, C₂ ∈ CAT, if:

•	KB, FD(C2)|FD(C1) and KB, FD(C1) FD(C2), then C1 implies C2 properly, or C2 is a proper subconcept of C1, denotation C2< C1 or IS-A(C2, C1)

With the definition of ≤ (<), all the properties of (or propositions about) C₁ are satisfied to C₂, which indicates the logical inheritance from C₁ to C₂. It is easy to prove that ≤ (<) relation satisfies transitivity and for any C₁, C₂ ∈ CAT, C₂ ≤ C₂ and C₁ ≤ C₂ if C₁ ≡ C₂.

Concept Overlapping
Definition 7: Let be a concept category. ∀C₁, C₂ ∈ CAT, C₁ and C₂ satisfy the relation of concept exclusion (denoted as C₂ ∝ C₁ or C₁ ∝ C₂), if there is a formula φ such that KB,φ|FD(C₁) and KB,φ|FD(C₂), but .

It is easy to prove that ∝ satisfies reflexivity, symmetry and non-transitivity. Besides, relation ∝ satisfies the following proposition.

Proposition 2: Let be a concept category. ∀C₁, C₂ ∈ CAT such that C₃<C₂ and C₃<C₁, then C₂ ∝ C₁.

Proof: If there is a formula φ such that KB, FD(C₃)|φ, since C₃<C₂ and C₃<C₁, KB, FD(C₁)|φ and KB, FD(C₂)|φ. So, C₂ ∝ C₁.

The conclusion of Proposition 2 is obvious. Because C₃ is a subconcept of C₁ and C₂, C₃ is one of the overlapping parts of C₁ and C₂. For example, let C₁ be complemented lattice, C₂ be distributive lattice and C₃ be complemented distributive lattice, obviously C₁ and C₂ satisfy concept overlapping.

Concept exclusion
Definition 8: Let be a concept category. ∀C₁, C₂ ∈ CAT, C₁ and C₂ satisfy the relation of concept exclusion (denoted as C₁<≈>C₂), if there is a formula φ such that:

(2)	For any other formula φ', KB, φ φ' and KB, FD(C1)|φ' iff KB, FD(C2)|5φ'

Two concepts satisfying the relation of concept exclusion indicates that they are opposite in logic. Relation <≈> is a non-reflexivity, symmetry and transitivity relation and ∀C₁, C₂ ∈ CAT, C₁ and C₂ cannot satisfy ≡, � and ∝ if C₁ <≈> C₂. There are lots of concepts in mathematics satisfying the relation of concept exclusion, such as Commutative Group and Non-Commutative Group.

Concept weak-correlation: The four relations between concepts, concept equivalence, concept subsumption, concept overlapping, concept exclusion, indicate two concepts with same types have relations about their logical constraints. If two concepts with same types have no relations about their logical constraints, they are weak-correlation.

Definition 9: Let be a concept category. ∀C₁, C₂ ∈ CAT, C₁ and C₂ satisfy the relation of concept weak-correlation, if they do not satisfy ≡, �, ∝ or <≈>.

Two weak-correlation concepts are consistent only about their structures, but there no any relations about their logical constraints. When the concept categories are divided, it is not expected to put two weak-correlation concepts into one category, which can be overcome by refining the conditions for dividing categories. In this paper, we mainly discuss the inheritance relation to realize knowledge inheritance between concepts, so more details about the conditions for dividing categories are not considered here.

Five kinds of relations between concepts within a concept category are formally defined based on their intensions (or formal definitions).

Table 1:	Concept extension relations within a concept category

The extension relations between concepts within a concept category can be listed in Table 1.

THREE-LEVEL KNOWLEDGE INHERITANCE HIERARCHY OF MATHEMATICAL CONCEPTS

Based on the types of concepts, a given mathematical concept set can be divided into a set of concept categories. All the categories can be organized with the subcategory relation between categories, which can realize structural inheritance between concepts. Within a concept category, the concepts are organized based on the concept subsumption relation, which indicates the logical inheritance between concepts. Every concept includes a class of instances and all the instances satisfy the properties of the concept. Thus, a three-level knowledge inheritance hierarchy between mathematical concepts can be obtained, which is represented in Fig. 2. These three levels in the hierarchy are:

Fig. 2:	Three level hierarchy of mathematical concepts

Graph representation for knowledge inheritance hierarchy of mathematical concepts: The concept hierarchy can be represented by a directed graph. The inheritance graph of concept categories and the inheritance graph of concepts are defined respectively as follows.

Definition 10: G_CAT = <V_CAT, E_CAT, ξ> is an inheritance graph between concept categories iff:

•	is a concept category} is the vertex set of GCAT

Based on the definition of the inheritance graph between concept categories, G_CAT is a directed graph without any loops. ∀v_i, v_j, v_k ε V_CAT, ξ(v_i, v_k) = f ° g if ξ(v_i, v_j) = f and ξ(v_j, v_k) = g.

Definition 11: G = <V, E> is a concept inheritance graph iff:

We can represent the concept category inheritance and concept inheritance graph with one combined directed graph. The category vertex is represented by a big circle with a broken line and the inheritance relation between categories is represented by a directed arc with a broken line and every arc is labeled with the coercive function.

Fig. 3:	Directed graph representation for the concept hierarchy

For every big circle of category, the concept inheritance graph is embedded into it. The concept node is represented by a small circle and the inheritance relation between concepts is represented by a directed arc. Figure 3 shows an example.

Figure 3, the concept hierarchy is composed by three concept categories (CAT₁, CAT₂ and CAT₃). ξ(CAT₁, CAT₁, CAT₂) = f₁ and ξ(CAT₁, CAT₃) = f₂. In each concept category (CAT₁, CAT₂ or CAT₃), the concepts are organized by the inheritance relation.

AUTO-CONSTRUCTION ALGORITHM FOR KNOWLEDGE INHERITANCE HIERARCHY OF MATHEMATICAL CONCEPTS

Auto-construction algorithm: With the analysis for knowledge inheritance hierarchy between mathematical concepts, an auto-construction method for the hierarchy from concept knowledge base can be presented. According to the knowledge representation for the mathematical concepts, the Formal Definition (FD) in the knowledge frame presents the intension and the combination of parameters indicates the type of the concept. We can obtain the concept hierarchy with the knowledge frames of concepts if there are no errors in the frames. The auto-generation algorithm for knowledge inheritance hierarchy between mathematical concepts within NKIMath is presented in Algorithm 1.

Algorithm 1 only presents the framework for auto-generation of knowledge inheritance hierarchy between mathematical concepts within NKIMath. In Step 3 and 4, a reasoning machine is needed to judge the relations between concept categories or concepts.

A running example: In order to show the procedure of Algorithm 1, Table 2 presents the basic knowledge frames for concepts including Group, Ring, Non-associative Ring and so on, which only presents the main information in the knowledge frame, such as name, parameters and FD.

The procedure of auto-generation of the concept hierarchy in Table 2 is presented as in Fig. 4. With the first step, the KF (Knowledge Frame) of Group is read and a node (represented by the little circle in Fig. 4a for Group is produced and a node (represented by the big circle in Fig. 4a for GCC (Concept Category of Group) synchronously. Figure 4b shows the result after reading the KF of Ring. Fig. 4b, Ring is represented by the little circle and RCC (Concept Category of Ring) is represented by the big circle. Since GCC is inherited by RCC, a directed arc is represented from GCC to RCC. Figure 4 shows the whole procedure of the auto-generation of the concept knowledge inheritance hierarchy.

Fig. 4:	The procedure of auto-generation of the concept hierarchy

Table 2:	Knowledge frames of a set of concepts

RELATED WORK

Kerber and Kerber (1991) presented a frame-based knowledge representation method for mathematics and the main idea of which comes from object-oriented technology. Kerber and Kerber (1991), every frame is composed by name, a set of slots and fillers. Slot is a set of atom predicates and the filler of every slot is the value of the corresponding atom predicates. Figure 5 shows the knowledge representation for Group in Kerber and Kerber (1991).

Kerber’s frame-based knowledge representation for mathematics binds the related knowledge together, thus it is convenient for knowledge organization and maintenance. NKIMath enriched the information within the frame given by Kerber, which can satisfy more requirements of users. For example, IFD (Informal Definition) in natural language can be used for knowledge instruction or knowledge Q-A and knowledge translation patterns can be used for auto-generation of multi-lingual knowledge base to satisfy different requirements of users with different native language. In the frame given by Kerber, it is difficult to construct the knowledge inheritance hierarchy of mathematical concepts directly, so it is also difficult to realize knowledge inheritance between mathematical concepts. Within NKIMath, the knowledge inheritance between concepts can be realized by knowledge reasoning and the auto-construction algorithm for the hierarchy is given.

OMDoc is used for knowledge representation in many mathematical knowledge systems (Michael, 2001) and it will be accepted as the international standard for mathematical document marked language. The knowledge representation of NKIMath follows lots of similarities with OMDoc, for example, the FD and IFD attributes in NKIMath are corresponding to the FMP and CMP elements in OMDoc, respectively. However, the knowledge inheritance between concepts is also not defined by OMDoc. Although, OMDoc can provide hyperlink relation between, it is different from the knowledge inheritance relation between concepts and it is difficult to realize knowledge inheritance between concepts based on hyperlink relation.

Fig. 5:	Knowledge representation for group with kerber’s method

The hyperlink relation between concepts is based on the definitions of concepts provide by OMDoc, which is useful to acquire knowledge of concept according to the definition relations to ensure the knowledge complete. A concept-oriented knowledge acquisition method is given and adopted within NKIMath (Zeng et al., 2003).

A knowledge management environment for mathematical concepts within NKIMath, NKIMathE, has been developed to manage the acquired knowledge frames acquired (Zeng et al., 2004a, b). To auto-construct the knowledge inheritance hierarchy between concepts within NKIMath based on the algorithm presented in this study is one of the most important functions of NKIMathE. The knowledge inheritance hierarchy between concepts is convenient for knowledge browse, search and edit. According to the knowledge inheritance hierarchy between concepts, it is easy to discover the backbone about the concepts within NKIMath.

CONCLUSION AND FUTURE WORK

To realize knowledge inheritance between concepts is important to knowledge representation and acquisition of mathematical concepts. In this study, we introduce the knowledge inheritance mechanism between concepts within NKIMath and a three-level knowledge inheritance hierarchy and its auto-construction method are given. There are three main contributions in this study:

By now, we only consider the relations between concepts based on their formal definitions. In fact, there are many mathematical theorems (lemmas, propositions, etc.) that also build the relations between mathematical concepts. In the future, we will consider the knowledge representation and acquisition for mathematical theorems and have research on how to obtain relations between concepts with the knowledge of theorems. At the same time, a reasoning machine will be designed and developed to realize knowledge reasoning to construct the knowledge inheritance hierarchy automatically.