線性代數(shù)動態(tài)教科書系統(tǒng)的設(shè)計與實現(xiàn)

喬 宇，楊 靜

（1.廣西民族大學(xué) 信息科學(xué)與工程學(xué)院， 廣西 南寧 530006；2.廣西民族大學(xué) 軟件與信息安全學(xué)院， 廣西 南寧 530006；3.廣西混雜計算與集成電路設(shè)計分析重點實驗室，廣西 南寧 530006）

0 引 言

隨著“互聯(lián)網(wǎng)+”時代的到來，人們獲取知識和信息的方式越來越高效便捷。信息技術(shù)的飛速發(fā)展和移動互聯(lián)網(wǎng)的日益普及也促使教育行業(yè)迎來前所未有的變革。當(dāng)前教育信息化帶來的積極作用主要體現(xiàn)在增加學(xué)生與學(xué)生、學(xué)生與老師之間的互動以及借助網(wǎng)絡(luò)加快知識傳播。在當(dāng)前教學(xué)實踐中，教學(xué)手段的革新主要表現(xiàn)為教學(xué)活動的多媒體化。但學(xué)習(xí)者與教科書等靜態(tài)學(xué)習(xí)資源之間的交互缺陷卻沒有得到明顯改善?，F(xiàn)有的電子教科書大多仍以靜態(tài)形式呈現(xiàn)，僅提供最基本的瀏覽功能，不易呈現(xiàn)知識的內(nèi)在結(jié)構(gòu)與關(guān)系，用戶無法完成內(nèi)容修改和自動檢測等交互工作，難以實現(xiàn)知識層面的共享。此類電子教科書固然能滿足用戶最基本的學(xué)習(xí)需要，卻無法滿足個性化學(xué)習(xí)需求。因此開發(fā)智能化交互式電子教科書系統(tǒng)是我們應(yīng)當(dāng)研究并解決的問題。

電子教科書的智能化是指電子教材不僅能夠?qū)崿F(xiàn)基本的增、刪、改、查，還可進行復(fù)雜的數(shù)學(xué)計算與推理。近年來，符號計算和自動推理領(lǐng)域的學(xué)者們對智能電子教科書系統(tǒng)的實現(xiàn)進行了多方面探索性研究。王東明和陳肖宇等以幾何電子教科書為例，通過對幾何知識的形式化表述和管理[1,2]，設(shè)計并實現(xiàn)了一個幾何知識庫[3,4]，生成了一個初級版幾何動態(tài)教科書系統(tǒng)[5,6]。蔡川和蘇偉等對數(shù)學(xué)公式的表示轉(zhuǎn)化、搜索[7-9]等問題進行了研究，為智能教科書系統(tǒng)的開發(fā)提供了技術(shù)保障。

本文從線性代數(shù)知識管理的角度出發(fā)，根據(jù)教學(xué)中的實際需求，研究線性代數(shù)的知識數(shù)據(jù)管理問題，基于已有的符號計算與自動推理技術(shù)，設(shè)計并實現(xiàn)了一個初級版線性代數(shù)動態(tài)教科書系統(tǒng)，增加了用戶與教材之間的交互，進而方便線性代數(shù)課程的學(xué)習(xí)。

1 線性代數(shù)知識庫的設(shè)計與實現(xiàn)

線性代數(shù)知識庫是線性代數(shù)知識管理軟件的重要組成模塊，也是線性代數(shù)動態(tài)教科書系統(tǒng)的核心內(nèi)容，可為智能教學(xué)平臺提供數(shù)據(jù)支持。線性代數(shù)教材中所包含的數(shù)學(xué)定義、定理、公理等敘述性知識是線性代數(shù)知識庫的主要構(gòu)成部分，也是知識管理的主要內(nèi)容。應(yīng)不同用戶的使用需求，知識庫內(nèi)容需要用不同的形式表達(dá)，如形式化表示和自然語言表示等。由于線性代數(shù)相關(guān)軟件所需知識大抵相似，因此，構(gòu)建一個標(biāo)準(zhǔn)化的知識庫不僅可以滿足本系統(tǒng)的數(shù)據(jù)需要，也可為其他線性代數(shù)軟件提供數(shù)據(jù)支持。

1.1 線性代數(shù)知識的標(biāo)準(zhǔn)化

知識庫中內(nèi)容的呈現(xiàn)形式由線性代數(shù)軟件的需求決定，包括知識表述的語法檢查、自動翻譯和自動計算等。而要對線性代數(shù)知識進行處理，則要將知識封裝成不同的類型。在線性代數(shù)學(xué)科中，知識類型可分為定義、定理、引理、推論及證明等。由于線性代數(shù)的知識對象以敘述性內(nèi)容為主，且每一種知識類型可以包括多個知識對象，如不同的定義及定理等，因此，應(yīng)對線性代數(shù)知識數(shù)據(jù)進行詳細(xì)劃分，并從中提取出不同類型所對應(yīng)的數(shù)據(jù)項。

本文采用形式化語言表示知識數(shù)據(jù)，用其約束文本內(nèi)容語法，以便進行語法檢查，實現(xiàn)翻譯與自動推理功能。一階邏輯語言是描述數(shù)學(xué)知識最方便且強大的形式化語言，可用于描述由個體、函數(shù)及關(guān)系構(gòu)成的簡單數(shù)學(xué)命題和由簡單命題通過量詞和命題連接詞構(gòu)成的復(fù)雜命題以及命題之間的邏輯關(guān)系，在建立數(shù)學(xué)語言和數(shù)學(xué)推理的形式化系統(tǒng)過程中始終處于核心地位。在檢查邏輯公式的完整性時，一階邏輯的確可以起到比較有效的作用，但一階邏輯語言本身并不能表達(dá)知識的意義。因此在使用一階邏輯語言進行表述的基礎(chǔ)上，還需為知識數(shù)據(jù)的子語句與數(shù)據(jù)項添加類型約束，以便語法檢查。形式化表述的基本形式如下所示：

Type mathNoun（Type element1， Type element2，…）

Type Predicate（Type element1， Type element2，…）

線性代數(shù)知識表述中的名詞概念被形式化為名詞項，各名詞之間的關(guān)系形式化為謂詞語句，知識數(shù)據(jù)的形式化語言是由邏輯詞將形式化的數(shù)學(xué)概念名詞連接組成的語句。對線性代數(shù)知識數(shù)據(jù)的處理都以這些概念名詞為基本單位。線性代數(shù)概念的形式化表述中使用的名詞項與謂詞稱為詞匯（Vocabulary），而（Type element1， Type element2，……）稱為線性代數(shù)形式化表述的參數(shù)列表（AttributeList）。

有了知識對象的形式化表述，可按以下方法實現(xiàn)自動翻譯。翻譯過程包括以下兩個步驟：

（1）將各子語句中的概念名詞、邏輯連接詞翻譯為目標(biāo)語言、標(biāo)點符號或連接詞；

（2）將翻譯后的語句組合連接。

隨著知識庫的擴展，會產(chǎn)生更多復(fù)雜概念添加到知識庫中。這里的復(fù)雜概念是由簡單概念組合得到的新定義。因此，需要將簡單概念的形式化表述及翻譯對應(yīng)概念的腳本存儲于數(shù)據(jù)庫中。在對新插入的復(fù)雜概念進行自動翻譯時只需匹配詞匯與參數(shù)表，找到翻譯腳本來翻譯其中的簡單概念，進而將各簡單概念組合連接即可。除概念的詞匯及形式化表述的參數(shù)表外，還需設(shè)置知識類型中的其他屬性，包括以下幾種：

（1）Type： 形式化表述的線性代數(shù)概念類型；

（2）FormalDefinition：線性代數(shù)中概念的形式化表述；

（3）NaturalDefinition：線性代數(shù)中概念的自然語言表述，包括多種語言版本（如中文、英文等）的表述；

（4）FormalRepresentation：線性代數(shù)中其他知識對象的形式化表述；

（5）NaturalRepresentation：線性代數(shù)中知識對象的自然語言表述。

為滿足用戶基本的查詢需求，需設(shè)置以下屬性：

（1）KnowledgeName：線性代數(shù)知識對象的名字；

（2）KeyWords：線性代數(shù)知識對象的關(guān)鍵字。

（1）ObjectID：線性代數(shù)知識對象的唯一標(biāo)識符；

（2）UserName：知識對象創(chuàng)建者的用戶名。

1.2 線性代數(shù)知識庫設(shè)計與實現(xiàn)

1.2.1 線性代數(shù)知識對象之間的關(guān)系

設(shè)計知識庫的結(jié)構(gòu)必須理清線性代數(shù)知識對象之間的關(guān)系。這些關(guān)系類型可分為以下四種：

（1）線性代數(shù)概念之間的繼承關(guān)系（Inherit）。所有基本概念定義后，新概念的引入都來自基本概念。一個線性代數(shù)新概念由兩部分組成，即此概念的父概念和新特性。例如，由矩陣概念可引出方陣概念，除繼承矩陣的概念外，方陣的新特性是行數(shù)和列數(shù)相等。

（2）線性代數(shù)知識對象之間的語境關(guān)系（Context）。定義與知識對象之間可以構(gòu)成語境關(guān)系，這是線性代數(shù)教科書中最廣泛的關(guān)系。知識對象可以是定義、定理、公理、練習(xí)或命題對象。

（3）線性代數(shù)知識對象之間的導(dǎo)出關(guān)系（Derivation）。數(shù)學(xué)知識的積累就是以基本概念為基礎(chǔ)，經(jīng)邏輯推理而演繹出不同定理，進而生成龐大的數(shù)學(xué)知識庫。

（4）線性代數(shù)知識對象之間的關(guān)聯(lián)關(guān)系（Associate）。一個完整的知識點由定義、定理、推論等共同組成，這就是定理、定義等知識對象之間的關(guān)聯(lián)關(guān)系。

（4）我們將向“一帶一路”沿線發(fā)展中國家提供20億元人民幣緊急糧食援助，向南南合作援助基金增資10億美元，在沿線國家實施100個“幸福家園”、100個“愛心助困”、100個“康復(fù)助醫(yī)”等項目。我們將向有關(guān)國際組織提供10億美元落實一批惠及沿線國家的合作項目。

線性代數(shù)知識結(jié)構(gòu)即是所有知識對象之間關(guān)系的分類與集合。為清晰呈現(xiàn)知識對象之間的關(guān)系，現(xiàn)為知識庫結(jié)構(gòu)引入以下屬性：

（1）Precursor：表示線性代數(shù)知識對象的前件；

（2）Subcursor：表示線性代數(shù)知識對象的后件；

（3）RelationType：表示線性代數(shù)知識對象之間的關(guān)系。

1.2.2 知識庫的結(jié)構(gòu)設(shè)計與關(guān)系呈現(xiàn)

通過上述分析與設(shè)計實現(xiàn)了線性代數(shù)知識庫的建立，此知識庫能夠存儲和管理線性代數(shù)知識對象所封裝的線性代數(shù)知識數(shù)據(jù)。線性代數(shù)知識庫中的所有數(shù)據(jù)來自文獻(xiàn)。目前，有許多數(shù)據(jù)庫關(guān)系模型，從中選擇使用最廣泛、功能最強大的關(guān)系型數(shù)據(jù)模型作為知識庫的數(shù)據(jù)模型，并依據(jù)系統(tǒng)需求與表間的依賴關(guān)系設(shè)計知識對象模型。

知識對象之間的聯(lián)系通過可視化工具呈現(xiàn)。目前比較通用的可視化工具主要有GraphX，Gephi及Prefuse。但GraphX缺少較好的動態(tài)效果，Gephi更適合大型數(shù)據(jù)的關(guān)系呈現(xiàn)但不能詳細(xì)刻畫節(jié)點間的關(guān)系。而本系統(tǒng)的需求是體現(xiàn)各節(jié)點之間的關(guān)系，因此選擇Prefuse作為本系統(tǒng)的外接包。

Prefuse交互信息可視化可通過引用Java中可擴展的軟件框架Prefuse Toolkit實現(xiàn)。首先，將知識庫Knowledgemapnode表中的元素傳入到Table對象Node中；其次，將KOStructure表中的元素傳入到另一個Table對象Edge中；最后，Graph（）方法會根據(jù)Edge中的參數(shù)信息，將Node中的信息按照記錄好的關(guān)系模式顯示出來。本系統(tǒng)部分知識關(guān)系如圖1所示。

圖1 知識關(guān)系直觀圖

1.2.3 知識數(shù)據(jù)管理

線性代數(shù)知識庫使用數(shù)據(jù)庫管理系統(tǒng)MySQL Server作為數(shù)據(jù)管理工具，使用JavaSwing設(shè)計開發(fā)知識庫管理界面。知識數(shù)據(jù)管理界面如圖2所示。

圖2 系統(tǒng)知識管理界面

用戶可通過此界面增加、刪除以及修改定義、定理、引理、推論等知識對象所封裝的知識數(shù)據(jù)。由于線性代數(shù)的部分概念（如矩陣、線性方程組等）需要使用特殊格式才能在頁面呈現(xiàn)，因此需在管理界面上創(chuàng)建網(wǎng)頁版MathType鏈接，在MathType中編輯公式并轉(zhuǎn)化為MathML[10]代碼，瀏覽器讀取MathML代碼后即可正常顯示數(shù)學(xué)表達(dá)式。而目前只有Firefox瀏覽器能完全支持MathML的識別，因此產(chǎn)生的html文件只能通過Firefox瀏覽器運行。

知識庫為用戶提供查詢與瀏覽功能。用戶可通過關(guān)鍵字或知識名查詢知識庫中是否存在某些定義或定理所對應(yīng)的知識數(shù)據(jù)，并可對查詢到的知識數(shù)據(jù)進行修改。

2 線性代數(shù)動態(tài)教科書系統(tǒng)的人機交互界面及呈現(xiàn)

2.1 人機交互界面

傳統(tǒng)教科書編寫系統(tǒng)以文本形式進行線性編輯，生成的教科書最終以文本文檔的形式存儲。而采用文本編寫需在最終定稿前進行多次修改，特別是長篇幅的教科書在對內(nèi)容與結(jié)構(gòu)做修改時需要不斷對文檔進行查找與定位，而且對教科書內(nèi)容維護及處理的過程比較耗時。清晰的內(nèi)容結(jié)構(gòu)不僅可以增強文檔的可讀性，還可以幫助讀者根據(jù)結(jié)構(gòu)層次獲取知識內(nèi)容。

教科書的內(nèi)容通常被統(tǒng)一劃分為多個章節(jié)，每章內(nèi)容被劃分為若干節(jié)，每節(jié)按定義、定理、證明、例題、練習(xí)等進行知識分類?；谏鲜鼍€性代數(shù)知識數(shù)據(jù)的封裝與分類思想，同時為改進線性編輯模式缺陷，將教科書界面設(shè)計為由節(jié)點組成的樹形結(jié)構(gòu)，所有樹形節(jié)點按照教科書的“章-節(jié)”層次結(jié)構(gòu)分類，每個葉子節(jié)點表示不同的知識對象，并顯示知識類型名與知識名。每個節(jié)點所存儲的知識對象都有相應(yīng)的objectID值與之對應(yīng)，并鏈接到知識庫相關(guān)的知識數(shù)據(jù)中。因此，若用戶需要調(diào)整教科書結(jié)構(gòu)，則可直接對目錄樹進行操作，而對內(nèi)容的修改則通過節(jié)點轉(zhuǎn)化為對知識庫中知識數(shù)據(jù)的修改。

為方便對知識庫進行管理，線性代數(shù)動態(tài)教科書系統(tǒng)通過管理界面向用戶提供新建與維護教科書的操作，包括向樹形結(jié)構(gòu)目錄中添加、刪除或檢索節(jié)點，修改節(jié)點在知識庫中對應(yīng)的知識數(shù)據(jù)，任意拖動節(jié)點（特別地，當(dāng)子節(jié)點拖動到父節(jié)點的同級節(jié)點中時，此節(jié)點會成為另一個節(jié)點的子節(jié)點）等。

線性代數(shù)動態(tài)教科書系統(tǒng)還向用戶提供了智能化輔助功能。在用戶創(chuàng)建教科書的過程中，每一種操作都需經(jīng)過一定的處理以實現(xiàn)實時檢測的功能，確保教科書內(nèi)容的非冗余性、結(jié)構(gòu)一致性，并實現(xiàn)線性代數(shù)的自動計算。操作流程如圖3，圖4所示。

2.2 線性代數(shù)動態(tài)教科書的內(nèi)容呈現(xiàn)

用戶不僅可通過樹形目錄結(jié)構(gòu)調(diào)整教科書，修改其知識結(jié)構(gòu)與內(nèi)容，還可將教科書中的內(nèi)容以傳統(tǒng)的排版形式呈現(xiàn)出來，供瀏覽或打印。系統(tǒng)通過節(jié)點獲取相應(yīng)知識對象的ObjectID，用戶可根據(jù)自己的需求選擇目標(biāo)對象所封裝的知識內(nèi)容，再調(diào)用線性代數(shù)知識庫的瀏覽功能以生成可在瀏覽器中呈現(xiàn)所選知識內(nèi)容的html文件，文字排版可自動實現(xiàn)。

在實現(xiàn)文檔的自動呈現(xiàn)時，系統(tǒng)先將數(shù)據(jù)庫內(nèi)容通過程序轉(zhuǎn)換成xml文件，再通過XSL將xml文件轉(zhuǎn)換成html文件，這個過程即為XSLT（EXtensible Stylesheet Language Transformations，XSLT）。另外，系統(tǒng)還為用戶提供語言選擇功能，以便用戶實時切換教科書的顯示語言，使得教科書系統(tǒng)能夠便捷地構(gòu)建和維護不同語言版本的文檔。為便于用戶更好地理解文中出現(xiàn)的知識點，系統(tǒng)還為文檔中出現(xiàn)的知識名附加了鏈接，點擊可跳轉(zhuǎn)至知識名的詳細(xì)內(nèi)容頁。

圖4 拖動樹形目錄節(jié)點的操作流程

2.3 系統(tǒng)智能化功能的實現(xiàn)

2.3.1 語境關(guān)系自動推理

教科書所包含的知識內(nèi)容之間存在各種各樣的關(guān)系，而這些關(guān)系在組織教科書結(jié)構(gòu)以及安排教科書內(nèi)容中起著重要作用，其對教科書的構(gòu)建必不可少，因此，需將其作為元數(shù)據(jù)存儲在知識庫中。這些關(guān)系的獲取主要有兩種方式：一是在創(chuàng)建知識對象的同時用ObjectID創(chuàng)建相應(yīng)的聯(lián)結(jié)；二是根據(jù)線性代數(shù)知識數(shù)據(jù)的形式化表述自動推理出知識對象之間的關(guān)系。由于在線性代數(shù)的表述中概念的語義是由定義體現(xiàn)的，因此，概念與用以表述線性代數(shù)內(nèi)容的知識對象之間構(gòu)成了語境關(guān)系。

實現(xiàn)語境關(guān)系的自動推理要首先從知識庫中獲取線性代數(shù)概念（記為D）的形式化表述，其次通過程序處理將形式化語句中的括號、標(biāo)點符號、等號以及and，or，not或where等連接詞去掉，得出的結(jié)果即為與該概念形成語境關(guān)系的知識對象，最后將結(jié)果分別對應(yīng)的ObjectID值返回到用戶界面。繼承關(guān)系的自動發(fā)現(xiàn)則需檢測處理形式化語句后得到的結(jié)果中是否包含形如MathNoun1：FatherMathNoun或MathNoun2 where Predicate （Type element1， Type element2，…）的表述。若為前者，則繼承關(guān)系為D→Inherit fatherMathNoun；若為后者，則繼承關(guān)系為D→Inherit mathNoun2。返回結(jié)果如圖5所示。

圖5 知識關(guān)系的檢測結(jié)果

2.3.2 教科書內(nèi)容與結(jié)構(gòu)的自動檢測

用戶在構(gòu)建及使用教科書系統(tǒng)的過程中，增加、刪除及移動等操作會導(dǎo)致線性代數(shù)教科書內(nèi)容和結(jié)構(gòu)的變化。因此每次操作后，系統(tǒng)都會自動檢測與被操作的知識節(jié)點構(gòu)成語境關(guān)系的所有知識對象是否全部在此節(jié)點之前被定義過。若不是，則表明對此節(jié)點進行定義時所用到的知識對象中有未被定義的，或檢測之前的知識節(jié)點在進行定義時，組成語境關(guān)系的所有知識對象中是否有當(dāng)前節(jié)點；若有，則表明有知識對象在當(dāng)前節(jié)點在未被定義的情況下使用。上述兩種情況的發(fā)生都告訴用戶：修改或拖動的不合理導(dǎo)致教科書結(jié)構(gòu)出現(xiàn)了問題。例如，如果將矩陣概念從教科書中刪除或拖動至樹形結(jié)構(gòu)后，那么在教科書中表示單位矩陣概念以及其他以矩陣為父概念的目錄節(jié)點就會提示錯誤。在新建某知識對象并形成節(jié)點N1后，系統(tǒng)會檢測并返回與新添加知識有直接關(guān)系的知識對象集合，再查看知識庫中是否包含集合中的所有元素，若不全部包括則會提示添加缺少的知識對象，如圖6所示。點擊添加并生成節(jié)點N2后，若嘗試將節(jié)點N2拖動至N1后面或?qū)⒐?jié)點N1拖至N2前面，則導(dǎo)致教科書結(jié)構(gòu)不合理，節(jié)點顏色發(fā)生變化并提示出錯，如圖7所示。

圖6 推理出的未被定義知識對象

圖7 不合理拖動操作后的錯誤提示

2.4 線性代數(shù)的自動計算

自動計算頁面通過html，css技術(shù)結(jié)構(gòu)將用戶在html頁面中輸入的參數(shù)傳給JavaScript，由Sylvester完成計算過程并將結(jié)果返回到html界面實現(xiàn)。在html計算界面中，用戶輸入數(shù)據(jù)后點擊Compute按鈕，即可得出計算結(jié)果并返回界面。目前，計算界面可實現(xiàn)的計算有矩陣的求秩、逆、轉(zhuǎn)置、上上三角化、加、減、乘、方陣的行列式計算以及奇異矩陣的判定。

3 結(jié) 語

本文主要研究并實現(xiàn)了一個動態(tài)、交互、易維護的線性代數(shù)教科書智能系統(tǒng)。首先探究了線性代數(shù)知識庫的構(gòu)建及知識數(shù)據(jù)的形式化與結(jié)構(gòu)化，進而呈現(xiàn)了對線性代數(shù)知識數(shù)據(jù)進行管理的人機交互界面，最后展現(xiàn)了知識對象之間關(guān)系的自動發(fā)現(xiàn)、結(jié)構(gòu)一致性與內(nèi)容冗余性檢測及自動計算的實現(xiàn)過程。今后的研究工作主要包括三方面：一是改善線性代數(shù)知識庫的結(jié)構(gòu)設(shè)計使其應(yīng)用更為廣泛；二是為系統(tǒng)連接外部軟件以利用形式化語言調(diào)用其做更復(fù)雜的計算；三是優(yōu)化線性代數(shù)知識數(shù)據(jù)的處理算法以實現(xiàn)更智能化的功能。

[1] CHEN X Y， WANG D M.Formalization and specification of geometric knowledge objects[J]. Mathematics in computer science， 2013，7（4）：439-454.

[2] CHEN X Y， WANG D M.Management of geometric knowledge in textbooks[J]. Data & knowledge engineering， 2012（73）：43-57.

[3]王東明，黃熒，陳肖宇.幾何知識庫的設(shè)計與實現(xiàn)[J].計算機應(yīng)用，2009，29（2）：398-402.

[4] CHEN X Y， HUANG Y， WANG D M.On the design and implementation of a geometric knowledge base[C]. Post-proceedings of the 7th international workshop on automated deduction in geometry.berlin： Springer-Verlag， 2011.

[5]陳肖宇.電子幾何教科書系統(tǒng)的設(shè)計與實施[D].北京：北京航空航天大學(xué)，2011.

[6]CHEN X， ZHAO T， WANG D.GeoText：An intelligent dynamic geometry textbook[J]. ACM communications in computer algebra， 2013，46（3/4）：171-175.

[7] SU W， WANG P， LI L， et al.MathEdit， A browser-based visual mathematics expression editor[C].Proceedings of the 11th asian technology conference in mathematics，2006.

[8]蔡川，蘇偉，李廉.Presentation數(shù)學(xué)公式到Content轉(zhuǎn)換關(guān)鍵問題研究[J].計算機應(yīng)用與軟件，2012，29（8）： 30-33.

[9]陳立輝，蘇偉，蔡川，等.基于LaTex的Web數(shù)學(xué)公式提取方法研究[J].計算機科學(xué)，2014， 41（6）：148-154.

[10] BERT B. MathML [EB /OL].（2017-11-20） [2016-06-18]. http： //www. w3. org /Math /.

[11]蔣磊，吳孔逸，陳肖宇.幾何知識資源分享平臺的設(shè)計與實現(xiàn)[J].計算機應(yīng)用，2014，34（S1）：189-192.

[12] CHOU S C， GAO X S. Automated reasoning in geometry [C].Handbook of automated reasoning，2001.