A Classification Approach for Automated Reasoning Systems--A Case Study in Graph Theory

<p>Reasoning systems which create classifications of structured objects face the problem of how object descriptions can be used to reflect their components as well as relations among these components. Current reasoning systems on graph theory do not adequately provide models to discover complex relations among mathematical concepts (eg: relations involving subgraphs) mainly due to the inability to solve this problem. This thesis presents an approach to construct a knowledge-based system, GC (Graph Classification), which overcomes this difficulty in performing automated reasoning in graph theory. We describe graph concepts based on an attribute called Linear Recursive Constructivity (LRC). LRC defines classes by an algebraic formula supported by background knowledge of graph types. We use subsumption checking on decomposed algebraic expressions of graph classes as a major proof method. The search is guided by case-split-based inferencing. Using the approach GC has generated proofs for many theorems such as "any two distinct cycles (closed paths) having a common edge e contain a cycle not traversing e", "if cycle C1 contains edges e1, e2, and cycle C2 contains edges e2, e3, then there exists a cycle that contains e1 and e3" and "the union of a tree and a path is a tree if they have only a single common vertex."</p> <p>The main contributions of this thesis are: (1) Development of a classification-based knowledge representation and a reasoning approach for graph concepts, thus providing a simple model for structured mathematical objects. (2) Development of an algebraic theory for simplifying and decomposing graph concepts. (3) Development of a proof search and a case-splitting technique with the guidance of graph type knowledge. (4) Development of a proving mechanism that can be generate constructive proofs by manipulating only simple linear formalization of theorems.</p>

Name thesis:degree_name

Doctor of Philosophy (PhD)

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Year dc:date.available

1989

Author dc:creator

• Lin, Rong

Contributors dc:contributor

• Shunichi Toida
• Stephan Olariu
• Ravi Mukkamala
• Christian Wild

• Reasoning systems
• Classifications
• Graph theory
• Artificial Intelligence and Robotics

Statement dc:rights

• <p>In Copyright. URI: <a href="http://rightsstatements.org/vocab/InC/1.0/">http://rightsstatements.org/vocab/InC/1.0/</a> This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s).</p>

Repository record dc:identifier

https://digitalcommons.odu.edu/computerscience_etds/115

OAI identifier oai:identifier

oai:digitalcommons.odu.edu:computerscience_etds-1113