Coupling Ontology with Rule-Based Theorem Proving for Knowledge Representation and Reasoning

被引:0
作者
Zhong, Xiuqin [1 ]
Fu, Hongguang [1 ]
Jiang, Yan [1 ]
机构
[1] Univ Elect Sci & Technol China, Sch Comp Sci & Engn, Chengdu 610054, Sichuan, Peoples R China
来源
DATABASE THEORY AND APPLICATION, BIO-SCIENCE AND BIO-TECHNOLOGY | 2010年 / 118卷
关键词
Knowledge representation; Reasoning; Ontology; Rule-based; Theorem Proving; GEOMETRY;
D O I
暂无
中图分类号
Q81 [生物工程学(生物技术)]; Q93 [微生物学];
学科分类号
071005 ; 0836 ; 090102 ; 100705 ;
摘要
Theorem proving is an important topic in artificial intelligence. Several methods have already been proposed in this field, especially in geometry theorem proving. Since they belong to algebraic elimination method or artificial intelligence method, it is difficult to use them to express domain knowledge clearly or represent hierarchy of systems. Therefore, we build a loosely coupled system to combine ontology and rule-based reasoning. Firstly, we construct elementary geometry ontology with OWL DL by creating classes, properties and constraints for searching or reasoning in domains. Then we design bidirectional reasoning based on rules and reasoning strategies such as all-connection method, numerical test method, rule classification methods and so on for complex reasoning. The system greatly improves sharing and reusability of domain knowledge and simultaneously implements readable proofs for geometry theorem proving efficiently.
引用
收藏
页码:110 / 119
页数:10
相关论文
共 15 条
[1]  
[Anonymous], 1994, MACHINE PROOFS GEOME, DOI DOI 10.1142/9789812798152
[2]   A deductive database approach to automated geometry theorem proving and discovering [J].
Chou, SC ;
Gao, XS ;
Zhang, JZ .
JOURNAL OF AUTOMATED REASONING, 2000, 25 (03) :219-246
[3]  
Coelho H., 1986, Journal of Automated Reasoning, V2, P329, DOI 10.1007/BF00248249
[4]   Automated and readable simplification of trigonometric expressions [J].
Fu, Hongguang ;
Zhong, Xiuqin ;
Zeng, Zhenbing .
MATHEMATICAL AND COMPUTER MODELLING, 2006, 44 (11-12) :1169-1177
[5]  
HUANG YQ, 2009, ENV SCI INFORM APPL, V3, P381
[6]   USING GROBNER BASES TO REASON ABOUT GEOMETRY PROBLEMS [J].
KAPUR, D .
JOURNAL OF SYMBOLIC COMPUTATION, 1986, 2 (04) :399-408
[7]   GRAMY: A geometry theorem prover capable of construction [J].
Matsuda, N ;
Vanlehn, K .
JOURNAL OF AUTOMATED REASONING, 2004, 32 (01) :3-33
[8]   On the decidability and complexity of integrating ontologies and rules [J].
Rosati, R .
JOURNAL OF WEB SEMANTICS, 2005, 3 (01) :61-73
[9]  
Tarski A., 1951, A Decision Method for Elementary Algebra and Geometry
[10]   ELIMINATION PROCEDURES FOR MECHANICAL THEOREM-PROVING IN GEOMETRY [J].
WANG, DM .
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 1995, 13 (1-2) :1-24