Skip to main content
SpringerLink
Log in

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

  • Conference paper
Database Theory and Application, Bio-Science and Bio-Technology (BSBT 2010, DTA 2010)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 118))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Tarski, A.: Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)

    MATH  Google Scholar 

  2. Wen-Tsun, W.: Basic Principles of Mechanical Theorem Proving in Elementary Geometries. Journal of Automated Reasoning 2(3), 221–252 (1986)

    Article  Google Scholar 

  3. Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)

    Book  MATH  Google Scholar 

  4. Wang, D.M.: Elimination procedures for mechanical theorem proving in geometry. Annals of Mathematics and Artificial Intelligence 13(1-2), 1–24 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  5. Kapur, D.: Using Grobner bases to reason about geometry problems. Journal of Symbolic Computation 2(4), 399–408 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  6. Coelho, H., Pereira, L.M.: Automated reasoning in geometry theorem proving with Prolog. Journal of Automated Reasoning 2(4), 329–390 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  7. Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning 25(3), 219–246 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  8. Matsuda, N., Vanlehn, K.: GRAMY: A Geometry Theorem Prover Capable of Construction. Journal of Automated Reasoning 32(1), 3–33 (2004)

    Article  MathSciNet  Google Scholar 

  9. Zhang, J.Z., Gao, X.S., Chou, S.C.: Geometry Information Search System by Forward Reasoning. Chinese Journal of Computers 19(10), 721–724 (1996)

    Google Scholar 

  10. Zhang, J.Z., Li, C.Z.: Automatic Reasoning and Intellectual Platform of CAI Software. Journal of Guangzhou University 15(2) (2001)

    Google Scholar 

  11. Wu, W.Y., Zeng, Z.B., Fu, H.G.: Designing Knowledge Base for the Elementary Geometry Based on Ontology. Computer Applications 22(3), 10–14 (2002)

    Google Scholar 

  12. Zhong, X.Q., Fu, H.G., She, L., Huang, B.: Geometry Knowledge Acquisition and Representation on ontology. Chinese Journal of Computers 33(1), 167–174 (2010)

    Article  Google Scholar 

  13. Huang, Y.Q., Deng, G.Y.: Research on Representation of Geographic Spatio-temporal Information and Spatio-temporal Reasoning Rules Based on Geo-ontology and SWRL. Environmental Science and Information Application Technology 3, 381–384 (2009)

    Google Scholar 

  14. Rosati, R.: On the decidability and complexity of integrating ontologies and rules. Journal of Web Semantics 3(1), 61–73 (2005)

    Article  Google Scholar 

  15. Fu, H.G., Zhong, X.Q., Zeng, Z.B.: Automated and Readable Simplification of Trigonometric Expressions. Mathematical and Computer Modeling 44, 1169–1177 (2006)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, University of Electronic Science and Technology of China, Chengdu, 610054, China

    Xiuqin Zhong, Hongguang Fu & Yan Jiang

Authors
  1. Xiuqin Zhong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hongguang Fu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yan Jiang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Victoria University, 8001, Melbourne, VIC, Australia

    Yanchun Zhang

  2. University of Calabria, Via P. Bucci, 41C, I-87036, Rende, Cosenza, Italy

    Alfredo Cuzzocrea

  3. Hosei University, 3-7-2, Kajino-cho, Koganei-shi, 184-8584, Tokyo, Japan

    Jianhua Ma

  4. Information Security Infrastructure Research Group, Electronics and Telecommunications Research Institute, 161, Gajeong-Dong, Yuseong-Gu, Daejeon, Korea

    Kyo-il Chung

  5. Engineering and Electronics, Edinburgh University, King’s Buildings, Faraday, rm 3.101, Mayfield Road, EH9 3JL, Edinburgh, UK

    Tughrul Arslan

  6. Nanjing University of Aeronautics and Astronautics, 210016, Jiangsu, Nanjing, China

    Xiaofeng Song

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhong, X., Fu, H., Jiang, Y. (2010). Coupling Ontology with Rule-Based Theorem Proving for Knowledge Representation and Reasoning. In: Zhang, Y., Cuzzocrea, A., Ma, J., Chung, Ki., Arslan, T., Song, X. (eds) Database Theory and Application, Bio-Science and Bio-Technology. BSBT DTA 2010 2010. Communications in Computer and Information Science, vol 118. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17622-7_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17622-7_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17621-0

  • Online ISBN: 978-3-642-17622-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation