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.\"
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.
","abstract_html":"<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>","abstract_has_math":false,"creators":["Lin, Rong"],"institution":null,"degree_name":"Doctor of Philosophy (PhD)","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Shunichi Toida","Stephan Olariu","Ravi Mukkamala","Christian Wild"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":1989,"date_issued":"1989-04-01T08:00:00Z","date_published":"1989-04-01T08:00:00Z","updated_at":"2026-07-24T03:35:15Z","subjects":["Reasoning systems","Classifications","Graph theory","Artificial Intelligence and Robotics"],"languages":[],"rights":["In Copyright. URI: http://rightsstatements.org/vocab/InC/1.0/ 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).
"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://digitalcommons.odu.edu/computerscience_etds/115","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Shunichi Toida","Stephan Olariu","Ravi Mukkamala","Christian Wild"]},{"key":"dc:creator","label":"Author","values":["Lin, Rong"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.available","label":"Dc Date Available","values":["2019-10-03T07:00:00Z"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Reasoning systems","Classifications","Graph theory","Artificial Intelligence and Robotics"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright. URI: http://rightsstatements.org/vocab/InC/1.0/ 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).
"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://digitalcommons.odu.edu/computerscience_etds/115"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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.\"
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.
"]},{"key":"dc:title","label":"Title","values":["A Classification Approach for Automated Reasoning Systems--A Case Study in Graph Theory"]}]}],"canonical_facts":{"dc:contributor":["Shunichi Toida","Stephan Olariu","Ravi Mukkamala","Christian Wild"],"dc:creator":["Lin, Rong"],"dc:date.available":["2019-10-03T07:00:00Z"],"dc:description.abstract":["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.\"
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.
"],"dc:identifier":["https://digitalcommons.odu.edu/computerscience_etds/115"],"dc:rights":["In Copyright. URI: http://rightsstatements.org/vocab/InC/1.0/ 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).
"],"dc:subject":["Reasoning systems","Classifications","Graph theory","Artificial Intelligence and Robotics"],"dc:title":["A Classification Approach for Automated Reasoning Systems--A Case Study in Graph Theory"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-24T03:35:15Z"}