Article

Reasoning support for expressive ontology languages using a theorem prover

Authors:

Andrei VoronkovAuthors Info & Claims

FoIKS'06: Proceedings of the 4th international conference on Foundations of Information and Knowledge Systems

Pages 201 - 218

https://doi.org/10.1007/11663881_12

Published: 14 February 2006 Publication History

Abstract

It is claimed in [45] that first-order theorem provers are not efficient for reasoning with ontologies based on description logics compared to specialised description logic reasoners. However, the development of more expressive ontology languages requires the use of theorem provers able to reason with full first-order logic and even its extensions. So far, theorem provers have extensively been used for running experiments over TPTP containing mainly problems with relatively small axiomatisations. A question arises whether such theorem provers can be used to reason in real time with large axiomatisations used in expressive ontologies such as SUMO. In this paper we answer this question affirmatively by showing that a carefully engineered theorem prover can answer queries to ontologies having over 15,000 first-order axioms with equality. Ontologies used in our experiments are based on the language KIF, whose expressive power goes far beyond the description logic based languages currently used in the Semantic Web.

References

[1]

L. Bachmair and H. Ganzinger. Resolution theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 2, pages 19-99. Elsevier Science, 2001.

[2]

S. Bechhofer, I. Horrocks, C. Goble, and R. Stevens. OilEd: A reason-able ontology editor for the semantic web. In F. Baader, G. Brewka, and T. Eiter, editors, KI 2001: Advances in Artificial Intelligence, volume 2174 of Lecture Notes in Computer Science, pages 396-408. Springer Verlag, 2001.

Digital Library

[3]

S. Bechhofer, F. van Harmelen, J. Hendler, I. Horrocks, D. L. McGuinness, P. F. Patel-Schneider, and L. A. Stein. OWL web ontology language 1.0 reference. W3C Recommendation, 10 February 2004. Available at http://www.w3.org/TR/owl-ref/.

[4]

D. Berardi, M. Grüninger, R. Hull, and S. McIlraith. Towards a first-order ontology for semantic web services. http://www.w3.org/2004/08/ws-cc/mci-20040904, sep 2004.

[5]

T. Berners-Lee, J. Hendler, and O. Lassila. The semanticWeb. Scientific American, 284(5):34-43, 2001.

[6]

H. Boley, M. Dean, B. Grosof, M. Sintek, B. Spencer, S. Tabet, and G. Wagner. First-Order-Logic RuleML. http://www.ruleml.org/fol/, 2004.

[7]

K. Claessen and N. Sörensson. New techniques that improve mace-style model finding. In Proceedings of the Workshop Model Computation 2003, 2003.

[8]

A. Degtyarev, R. Nieuwenhuis, and A. Voronkov. Stratified resolution. Journal of Symbolic Computations, 36(1-2):79-99, 2003.

Digital Library

[9]

A. Emmen. The grid needs ontologies-onto-what?, 2002. http://www.hoise.com/primeur/03/articles/monthly/AE-PR-02-03-7.html.

[10]

R. Fikes, P. Hayes, and I. Horrocks. OWL-QL-a language for deductive query answering on the Semantic Web. Journal of Web Semantics, 2004. To Appear.

Digital Library

[11]

I. Foster, C. Kesselman, J. Nick, and S. Tuecke. The physiology of the grid: An open grid services architecture for distributed systems integration, 2002. http://www.globus.org/research/papers/ogsa.pdf.

[12]

H. Ganzinger and J. Stuber. Superposition with equivalence reasoning and delayed clause normal form transformation. In F. Baader, editor, 19th International Conference on Automated Deduction (CADE-19), volume 2741 of Lecture Notes in Computer Science, pages 335-349. Springer Verlag, 2003.

[13]

V. Haarslev and R. Möller. RACER User's Guide and Reference Manual. Version 1.7.7, Sept. 2003.

[14]

P. Hayes and C. Menzel. A semantics for the knowledge interchange format. In IJCAI 2001 Workshop on the IEEE Standard Upper Ontology, 2001.

[15]

I. Horrocks. Using an expressive description logic: FaCT or fiction? In A. Cohn, L. Schubert, and S. Shapiro, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR'98), pages 636- 647, San Francisco, CA, June 1998. Morgan Kaufmann.

[16]

I. Horrocks, L. Li, D. Turi, and S. Bechhofer. The instance store: DL reasoning with large numbers of individuals. In Proc. of the 2004 Description Logic Workshop (DL 2004), pages 31-40, 2004.

[17]

I. Horrocks and P. F. Patel-Schneider. A proposal for an OWL rules language. In Proc. of the Thirteenth International World Wide Web Conference (WWW 2004), pages 723-731. ACM, 2004.

Digital Library

[18]

I. Horrocks, P. F. Patel-Schneider, H. Boley, S. Tabet, B. Grosof, and M. Dean. SWRL: A semantic web rule language combining owl and ruleml. W3C Note, 21 May 2004. Available at http://www.w3.org/Submission/SWRL/.

[19]

I. Horrocks, P. F. Patel-Schneider, and F. van Harmelen. Reviewing the design of DAML+OIL: An ontology language for the semantic web. In Proc. of the 18th National Conference on Artificial Intelligence (AAAI 2002), pages 792-797. AAAI Press, 2002.

Digital Library

[20]

I. Horrocks, P. F. Patel-Schneider, and F. van Harmelen. From SHIQ and RDF to OWL: The making of a web ontology language. Journal of Web Semantics, 1(1):7-26, 2003.

[21]

I. Horrocks and U. Sattler. The effect of adding complex role inclusion axioms in description logics. In Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003), pages 343-348. Morgan Kaufmann, 2003.

Digital Library

[22]

I. Horrocks and S. Tessaris. Querying the semantic web: a formal approach. In I. Horrocks and J. Hendler, editors, First International Semantic Web Conference (ISWC 2002), number 2342 in Lecture Notes in Computer Science, pages 177-191. Springer Verlag, 2002.

Digital Library

[23]

U. Hustadt, B. Konev, A. Riazanov, and A. Voronkov. TeMP: A temporal monodic prover. In M. R. D.A. Basin, editor, Automated Reasoning - Second International Joint Conference, IJCAR 2004, volume 3097 of Lecture Notes in Computer Science, pages 326-330. Springer Verlag, 2004.

[24]

U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. In I. P. Gent, H. van Maaren, and T. Walsh, editors, SAT 2000: Highlights of Satisfiability Research in the Year 2000, volume 63 of Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, 2000. Also to appear in a special issue of Journal of Automated Reasoning.

Digital Library

[25]

P. P.-S. I. Horrocks. Three theses of representation in the semantic web. In Proceedings of the Twelfth International World Wide Web Conference, WWW2003, pages 39-47, Budapest, Hungary, Jan. 2003. ACM.

Digital Library

[26]

T. Kutsia. Theorem proving with sequence variables and flexible arity symbols. In M.Baaz and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002), volume 2514 of Lecture Notes in Artificial Intelligence, pages 278-291, Tbilisi, Georgia, 2002.

Digital Library

[27]

W. McCune. Mace4 reference manual and guide. Technical Memorandum 264, Argonne National Laboratory, Aug. 2003.

[28]

W. McCune. OTTER 3.3 reference manual. Technical Memorandum 263, Argonne National Laboratory, Aug. 2003.

[29]

P. Mika, D. Oberle, A. Gangemi, and M. Sabou. Foundations for service ontologies: Aligning OWL-S dolce. In S. Feldman, M. Uretsky, M. Najork, and C. Wills, editors, WWW 2004, Proceedings of the 13th international conference on World Wide Web, pages 563-572. ACM, 2004.

Digital Library

[30]

A. Pease, I. Niles, and J. Li. The Suggested Upper Merged Ontology: A large ontology for the Semantic Web and its applications. In Working Notes of the AAAI-2002 Workshop on Ontologies and the Semantic Web, Edmonton, Canada, 2002.

[31]

Protégé. http://protege.stanford.edu/, 2003.

[32]

A. Rector. Analysis of propagation along transitive roles: Formalisation of the galen experience with medical ontologies. In Proc. of DL 2002. CEUR (http://ceur-ws.org/), 2002.

[33]

A. Rector, S. Bechhofer, C. A. Goble, I. Horrocks, W. A. Nowlan, and W. D. Solomon. The Grail concept modelling language for medical terminology. Artificial Intelligence in Medicine, 9:139-171, 1997.

[34]

A. Rector and I. Horrocks. Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions. In Proc. of the 13th Nat. Conf. on Artificial Intelligence (AAAI 97), 1997.

[35]

A. Riazanov and A. Voronkov. The design and implementation of Vampire. AI Communications, 15(2-3):91-110, 2002.

Digital Library

[36]

A. Riazanov and A. Voronkov. Limited resource strategy in resolution theorem proving. Journal of Symbolic Computations, 36(1-2):101-115, 2003.

Digital Library

[37]

S. Schulz and U. Hahn. Parts, locations, and holes - formal reasoning about anatomical structures. In Proc. of AIME 2001, volume 2101 of Lecture Notes in Artificial Intelligence. Springer Verlag, 2001.

Digital Library

[38]

Common Logic Standard. http://cl.tamu.edu/.

[39]

R. Sekar, I. Ramakrishnan, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 26, pages 1853-1964. Elsevier Science, 2001.

Digital Library

[40]

K. Spackman. Managing clinical terminology hierarchies using algorithmic calculation of subsumption: Experience with snomed-rt. J. of the Amer. Med. Informatics Ass., 2000. Fall Symposium Special Issue.

[41]

R. Stevens, C. Goble, I. Horrocks, and S. Bechhofer. Building a bioinformatics ontology using OIL. IEEE Transactions on Information Technology in Biomedicine, 6(2):135-141, 2002.

Digital Library

[42]

T. Tammet. Completeness of resolution for definite answers. Journal of Logic and Computation, 5(4):449-471, 1995.

[43]

T. Tammet. Gandalf. Journal of Automated Reasoning, 18(2):199-204, 1997.

Digital Library

[44]

The DAML Services Coalition. DAML-S: Web service description for the semantic web. In Proc. of the 2003 International Semantic Web Conference (ISWC 2003), number 2870 in Lecture Notes in Computer Science. Springer Verlag, 2003.

Digital Library

[45]

D. Tsarkov, A. Riazanov, S. Bechhofer, and I. Horrocks. Using Vampire to reason with OWL. In Semantic Web 2004. Springer Verlag, 2004. to appear.

[46]

S. Tuecke, K. Czajkowski, I. Foster, J. Frey, S. Graham, C. Kesselman, and P. Vanderbilt. Grid service specification (draft). GWD-I draft, GGF Open Grid Services Infrastructure Working Group, 2002.

[47]

M. Uschold, M. King, S. Moralee, and Y. Zorgios. The enterprise ontology. Knowledge Engineering Review, 13, 1998.

Digital Library

[48]

F. van Harmelen, P. F. Patel-Schneider, and I. Horrocks. Reference description of the DAML+OIL (March 2001) ontology markup langauge, Mar. 2001.

[49]

A. Voronkov. k K: a theorem prover for K. In H. Ganzinger, editor, Automated Deduction-CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 383-387, Trento, Italy, July 1999.

Digital Library

Cited By

Sharma AGoolsbey K(2019)Simulation-based approach to efficient commonsense reasoning in very large knowledge basesProceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v33i01.33011360(1360-1367)Online publication date: 27-Jan-2019
https://dl.acm.org/doi/10.1609/aaai.v33i01.33011360
Dundua BKutsia TRukhaia M(2019)Unranked Nominal UnificationLanguage, Logic, and Computation10.1007/978-3-030-98479-3_14(279-296)Online publication date: 16-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-98479-3_14
Sharma AGoolsbey KSingh SMarkovitch S(2017)Identifying useful inference paths in large commonsense knowledge bases by retrograde analysisProceedings of the Thirty-First AAAI Conference on Artificial Intelligence10.5555/3298023.3298211(4437-4443)Online publication date: 4-Feb-2017
https://dl.acm.org/doi/10.5555/3298023.3298211
Show More Cited By

Recommendations

The Watson Theorem Prover

Watson is a general-purpose system for formal reasoning. It is an interactive equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive in being type free (it is a safe variant of Quine's i>NF). Watson ...
Theorem Prover for Intuitionistic Logic Based on the Inverse Method

The first-order intuitionistic logic is a formal theory from the family of constructive logics. In intuitionistic logic, it is possible to extract a particular example x = a and a proof of a formula P(a) from a proof of a formula źxP(x). Owing to this ...
Verified heap theorem prover by paramodulation
ICFP '12

We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked static analyses ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FoIKS'06: Proceedings of the 4th international conference on Foundations of Information and Knowledge Systems

February 2006

331 pages

ISBN:3540317821

Editors:
Jürgen Dix
Clausthal University of Technology, Julius-Albert-Str. 4, Clausthal-Zellerfeld, Germany
,
Stephen J. Hegner
Department of Computing Science, Umeå University, Julius-Albert-Str. 4, Umeå, Sweden

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 14 February 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sharma AGoolsbey K(2019)Simulation-based approach to efficient commonsense reasoning in very large knowledge basesProceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v33i01.33011360(1360-1367)Online publication date: 27-Jan-2019
https://dl.acm.org/doi/10.1609/aaai.v33i01.33011360
Dundua BKutsia TRukhaia M(2019)Unranked Nominal UnificationLanguage, Logic, and Computation10.1007/978-3-030-98479-3_14(279-296)Online publication date: 16-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-98479-3_14
Sharma AGoolsbey KSingh SMarkovitch S(2017)Identifying useful inference paths in large commonsense knowledge bases by retrograde analysisProceedings of the Thirty-First AAAI Conference on Artificial Intelligence10.5555/3298023.3298211(4437-4443)Online publication date: 4-Feb-2017
https://dl.acm.org/doi/10.5555/3298023.3298211
Keet CKutz O(2017)Orchestrating a Network of Mereo(topo)logical TheoriesProceedings of the 9th Knowledge Capture Conference10.1145/3148011.3148013(1-8)Online publication date: 4-Dec-2017
https://dl.acm.org/doi/10.1145/3148011.3148013
Álvez JLucio PRigau GBarker KGómez-Pérez J(2015)Improving the Competency of First-Order OntologiesProceedings of the 8th International Conference on Knowledge Capture10.1145/2815833.2815841(1-8)Online publication date: 7-Oct-2015
https://dl.acm.org/doi/10.1145/2815833.2815841
Schneider MSutcliffe G(2011)Reasoning in the OWL 2 full ontology language using first-order automated theorem provingProceedings of the 23rd international conference on Automated deduction10.5555/2032266.2032301(461-475)Online publication date: 31-Jul-2011
https://dl.acm.org/doi/10.5555/2032266.2032301
Schneider M(2011)Reasoning in expressive extensions of the RDF semanticsProceedings of the 8th extended semantic web conference on The semanic web: research and applications - Volume Part II10.5555/2017936.2017983(487-491)Online publication date: 29-May-2011
https://dl.acm.org/doi/10.5555/2017936.2017983
Suda MWeidenbach CWischnewski P(2010)On the saturation of YAGOProceedings of the 5th international conference on Automated Reasoning10.1007/978-3-642-14203-1_38(441-456)Online publication date: 16-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-14203-1_38
Byrnes JBuchanan MErnst MMiller PRoberts CKeller R(2009)Visualizing Proof Search for Theorem Prover DevelopmentElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.12.095226(23-38)Online publication date: 1-Jan-2009
https://dl.acm.org/doi/10.1016/j.entcs.2008.12.095

View Options

View options

Media

Figures

Other

Tables

View Table of Contents