• Introduction
• GeoText

Manual

Installation

Unzip the package to your computer and double click GTextbook.jar to run GeoText (JDK 1.5 or JRE 1.5 or higher is required). Choose an "English" or "Chinese" version of the system to use and then log in the system by inputting your user name and password (for demonstrating the system, you can log in with a user name "Administrator" and password "123456"). New users should register by clicking New user button to create some basic information. Select a folder to install some configuration files while running the GeoText system.

Content Creation

Construct categories

Click the menu item File->New, and then a dialog box will be shown. Input the role of a category to be constructed in the form of "role(language)", such as "Textbook(english)", "Chapter(english)", or "节（中文）" to represent an English Textbook, an English chapter, or a Chinese section. Multiple versions of a role can be inputted by concatenating these versions with semicolons, such as "Section(english);节（中文）". In a similar way, input the name of the category (for identifying the category) and the title (for introducing the contents of the category). Multi-version contents of an introduction to the category can be constructed by editing in a tabbed textarea. A pop-up menu will be shown after right-click on the tabbed pane for you to manage the tabbed pages. For example, rename the tab of a new page to "中文" to represent the content is in Chinese. Keywords for querying the category can be inputted in the field Key Words. Finally, click OK to save the constructed subject contents of the category into the knowledge base.

An index tree will be shown afterwards with a subject object (rendered as a node) as its root. Select one node in the index tree and right-click will pop up a menu to show what operations can be performed on the selected node currently for constructing the index tree. For example, select the root node of a category and you can add a new node to the category; select any node and you can insert a new node before this node. These new nodes can be newly created into or queried from the knowledge base. You can also change the structure of an index tree by dragging the involved nodes. Finally, click the menu item File->Save to save the constructed index tree into the knowledge base.

Construct knowledge contents

Knowledge objects (rendered as leaf nodes), including Definitions, Axioms, Lemmas, Theorems, Corollaries, Conjectures, Proofs, Problems, Exercises, and Examples, can be constructed into the knowledge base, by clicking the corresponding toolbar buttons. Multi-version objects can be constructed through managing pages of the Advanced tabbed pane in the shown dialog boxes. You can select a tabbed page as default for rendering the object contents by clicking the pop-up menu item Set default for presentation. To make inputting convenient, item lists will be automatically shown under input fields for you to observe or select.

For a definition object, the fields Vocabulary and Attribute List constitute customized formalization of the defined concept, such as "circle" and "(Point,Point,Point)" respectively. Multiple versions of vocabulary can be inputted by concatenating these versions with semicolons, such as "circle;圆;kreis;cercle". The field Instance represents an instance of the concept to be defined, such as "circle(A::Point,B::Point,C::Point)", and the field Formal Definition contains the formalized content of the definition. The field Nondegeneracy Condition represents conditions under which the defined concept is meaningful, such as the three vertices of a triangle are not collinear. The field Natural Definition contains the definition content is in natural languages. Transformation rules for converting an instance of a formalized concept into statements in natural languages, algebraic representations, and instructions for drawing diagrams are constructed in the fields Translation Script, Algebraic Script, and Diagram Script, respectively. You can construct a dynamic diagram with GeoGebra by clicking Construct button, save it as a ".ggb" file to your computer, and then upload the file to the knowledge base by clicking Upload button. You can also browse your computer by clicking browse... button, upload an image file by dragging it into the Figure pane, and set a name for the image.

For a theorem object, the fields Hypothesis, Relation, and Conclusion constitute customized formalization of the theorem. The field Natural Representation contains the theorem content in natural languages. The field Algebraic Representation contains the data made up of algebraic expressions to specify the theorem under a coordinate system. The field Nondegeneracy Condition represents conditions under which the theorem is rigorously true. The field Diagram Instruction contains the data to be applied as commands for drawing or generating dynamic diagrams for the theorem configuration, such as GeoGebra construction commands concatenated with semicolons can be inputted for constructing the diagram in GeoGebra.

For a proof object, multi-version proofs can be constructed by managing tabbed pages in the Proof pane, such as a proof expressed in English or in Chinese.

For the other objects, contents can be similarly constructed into the corresponding fields.

Formalized data are specified by using Geometry Description Language (GDL) we have designed. Natural data can be described by using OpenMath format (OpenMath formulae can be created by clicking the button of formula editor in the tool bar and the formated representations can be acquired via the copy button.) or LaTeX syntax (for mathematical formulae) and XHTML format, and by copying specific representations through clicking the menu items of Tools->Style and Tools->Symbol.

Construct relations

Relations can be constructed by managing tabbed pages in the Relation pane. Each tabbed page contains relations with the type selected from the box Relation Type. You can input the corresponding IDs (assigned to objects by the system) of objects related with the currently constructed object in the fields Precursor and Subsequence. Conveniently, a list of object IDs will be shown for you to select by just inputting the role of an object into these two fields.

There are 16 types of relations among objects already defined the current system and you can also defined a new relation type by inputting its name in the field Relation Type. The meanings and usages of built-in relations can be found here.

Content Maintenance

Set a user context

A user context indicates that objects contributed by which user are visible for you. When you log in the system, the default user context is yourself and you have all privileges of creating, modifying, and removing your own contributions. Click the menu Context->Users and then you can change the current user context by selecting another user name. Then you have the privileges of querying, viewing, and reusing objects contributed by this user.

Open index trees

Click the menu item File->Open and input the role and name of an object in the shown dialog box, then an index tree with this object as the root will be generated. For example, input "Textbook(english)" into the field Role and "Geometry Revisited(english)" into the field Name and then click OK, an index tree representing the textbook "Geometry Revisited" will be shown. You can open many index trees shown in a tabbed pane.

Query

Click the menu item Query->Browse the Knowledge Base, input specific query commands, and click Query button, the results matched from the knowledge base under the current user context will be then shown as an index tree.

Click the menu item Query->Query the Textbook, input specific query commands, and click Query button, the results matched in the current shown index tree will be highlighted.

The commands include

• browseBy[R,N], where R is the role of required objects (such as Chapter, Section, Definition, or Theorem) and N is the name of required objects (such as Simson lines or Simson's theorem);
• keyWords[S], where S is the key word of required objects.

R, N, and S can also be wildcard "*" or be connected by "and", "or", "not" in the form of "and(...,...)", "or(...,...)", "not(...)".

Consistency checking

Click the menu Intelligence->Consistency Checking, select the needed relation types for consistency checking, and then in the process of maintaining index trees, the system will automatically

• check whether a new node can be appropriately added or inserted into a chosen position, whether a node is still in an appropriate position after its content is modified, whether a node can be moved from one position to another, and whether a node can be removed from the index tree (and highlighting the nodes that disallow the operations);
• generate a list of prerequisite nodes when a new node is added or inserted, or the content of a node is modified (for the user to determine and select the needed nodes to be added into the textbook);
• check whether a node to be added or inserted already exists in the textbook.

Content Rendering

Select the root or a branch node in an index tree and click View in a pop-up menu, a web page will be generated to render the default contents of the selected node and its children nodes. You can also select more than one node to produce the document. To render mathematical objects therein, your browser is required to install some plug-in to display MathML objects, such as MathPlayer.

Click the menu Preference->Language and select "English" or "中文", then the system will dynamically change its working language in real time.

Click Show structure button, and then a dynamic labeled graph will be shown to render relations among the nodes stored in the knowledge base. Click Show Tree button, and then a dynamic tree will be shown to render index trees stored in the knowledge base.

Knowledge Processing

The following functionalities depend on the inputted formalized data and may not work in all cases. They may also take some time to generate the results.

Relation discovering

Click the menu Intelligence->Relation Discovering, select the needed relation types for automatically discovering relations among nodes, and then in the process of creating and modifying the content of a knowledge object, the system will analyze its formalized data and automatically generate a list of objects related with this object for you to select to add these relations into the knowledge base.

Theorem proving

To use this functionality, your computer is required to install GEOTHER.

Click Auto-Prove->Use GEOTHER in a pop-up menu on an index tree, the selected object will be automatically proved. The proof and proving results will be recorded in a document shown to you.

Diagram generation

Click Auto-Draw->Use GeoGebra in a pop-up menu on an index tree, a web page will be shown to you. Click Auto-draw button in the page and a dynamic diagram will be constructed step by step automatically. During this process, you can drag the constructed points to interactively change the figure. Click Pause and Continue buttons to pause and continue the construction process. Click Restart button to redo the construction process. Click Objective button to highlight what geometric relations are being investigated in the diagram.

Click Auto-Draw->Use GeoDraw in a pop-up menu on an index tree, a dynamic diagram for the configuration of the selected object will be automatically generated.