Abstract
OWL DL corresponds to a Description Logic (DL) that is a fragment of classical first-order predicate logic (FOL). Therefore, the standard methods of automated reasoning for full FOL can potentially be used instead of dedicated DL reasoners to solve OWL DL reasoning tasks. In this paper we report on some experiments designed to explore the feasibility of using existing general-purpose FOL provers to reason with OWL DL. We also extend our approach to SWRL, a proposed rule language extension to OWL.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2002)
Baader, F., Hollunder, B., Nebel, B., Profitlich, H.-J., Franconi, E.: An empirical analysis of optimization techniques for terminological representation systems. In: Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 1992), pp. 270–281. Morgan Kaufmann, Los Altos (1992)
Bachmair, L., Ganzinger, H.: ResolutionTheorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 2, pp. 19–99. Elsevier Science, Amsterdam (2001)
Baker, P.G., Brass, A., Bechhofer, S., Goble, C., Paton, N., Stevens, R.: Tambis: Transparent access to multiple bioinformatics information sources: an overview. In: Proceedings of the Sixth International Conference on Intelligent Systems for Molecular Biology, ISMB 1998, pp. 25–34. AAAI Press, Menlo Park (1998)
Biron, P.V., Malhotra, A.: XML schema part 2: Datatypes. W3C Recommendation (May 2001), http://www.w3.org/TR/xmlschema-2/
Borgida, A.: On the relative expressiveness of description logics and predicate logics. Artificial Intelligence 82(1-2), 353–367 (1996)
The CASC web page, http://www.cs.miami.edu/~tptp/CASC/
Dean, M., Connolly, D., van Harmelen, F., Hendler, J., Horrocks, I., McGuinness, D.L., Patel-Schneider, P.F., Stein, L.: OWLWebOntology Language Reference. W3C Recommendation, February 10 (2004), http://www.w3.org/TR/owl-ref/
DL 1998 test suite, http://dl.kr.org/dl98/comparison/
Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proc. IEEE Conference on Logic in Computer Science (LICS), pp. 295–304 (1999)
Genesereth, M.R., Fikes, R.E.: Knowledge Interchange Format Version 3.0 Reference Manual. Technical Report Logic Group Report Logic-92-1, Stanford University (2001), http://logic.stanford.edu/kif/Hypertext/kif-manual.html
Gradel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proceedings of LICS 1997, pp. 306–317 (1997)
Horrocks, I., Patel-Schneider, P.F., Boley, H., Tabet, S., Grosof, B., Dean, M.: SWRL: A SemanticWeb Rule Language Combining OWL and RuleML (2003), http://www.daml.org/2003/11/swrl/
Horrocks, I., Tobies, S.: Reasoning with axioms: Theory and practice. In: Proc. of the 7th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 2000), pp. 285–296 (2000)
Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Proc. of the 6th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 1998), pp. 636–647 (1998)
Horrocks, I., Patel-Schneider, P.F.: The generation of DAML+OIL. In: Proc. of the 2001 Description Logic Workshop (DL 2001). CEUR Electronic Workshop Proceedings, pp. 30–35 (2001), http://ceur-ws.org/Vol-49/
Horrocks, I., Patel-Schneider, P.F.: Reducing OWL entailment to description logic satisfiability. In: Fensel, D., Sycara, K., Mylopoulos, J. (eds.) ISWC 2003. LNCS, vol. 2870, pp. 17–29. Springer, Heidelberg (2003)
Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In: Proc. of the 17th Int. Joint Conf. on Artificial Intelligence (IJCAI 2001), pp. 199–204 (2001)
Horrocks, I., Sattler, U.: The effect of adding complex role inclusion axioms in description logics. In: Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003), pp. 343–348. Morgan Kaufmann, Los Altos (2003)
Hustadt, U., Schmidt, R.A.: MSPASS: Modal reasoning by translation and first-order resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 67–71. Springer, Heidelberg (2000)
Levy, A.Y., Rousset, M.-C.: CARIN: A representation language combining horn rules and description logics. In: European Conference on Artificial Intelligence, pp. 323–327 (1996)
Mortimer, M.: On languages with two variables. Zeitschr. für math. Logik und Grundlagen der Math. 21, 135–140 (1975)
Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., Mayr, K.: SETHEO and e-SETHEO - the CADE-13 systems. Journal of Automated Reasoning 18(2), 237–246 (1997)
Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch.7, pp. 371–443. Elsevier Science, Amsterdam (2001)
OWL test suite, http://www.w3.org/TR/owl-test/
Paramasivam, M., Plaisted, D.A.: Automated deduction techniques for classification in description logic systems. J. of Automated Reasoning 20(3), 337–364 (1998)
Patel-Schneider, P.F., Hayes, P., Horrocks, I.: OWL web ontology language semantics and abstract syntax. W3C Recommendation, February 10 (2004), Available at http://www.w3.org/TR/owl-semantics/
Rector, A.L., Nowlan, W.A., Glowinski, A.: Goals for concept representation in the galen project. In: Proc. of the 17th Annual Symposium on Computer Applications in Medical Care (SCAMC’93), Washington DC, USA, pp. 414–418 (1993)
Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)
Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI 1991), pp. 466–471 (1991)
Sutcliffe, G., Suttner, C.: The TPTP Problem Library. TPTP v. 2.4.1. Technical report, University of Miami (2001)
Sutcliffe, G., Suttner, C.: The TPTP Problem Library. TPTP v. 2.4.1. Technical report, University of Miami (2001)
Tammet, T.: Gandalf. Journal of Automated Reasoning 18(2), 199–204 (1997)
Tammet, T.: Extending Classical Theorem Proving for the Semantic Web. In: Volz, R., Decker, S., Cruz, I. (eds.) Proceedings of the First International Workshop on Practical and Scalable Semantic Systems (October 2003), http://km.aifb.uni-karlsruhe.de/ws/psss03/proceedings
Tobies, S.: Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, LuFG Theoretical Computer Science, RWTH-Aachen, Germany (2001)
Tsarkov, D., Horrocks, I.: DL reasoner vs. first-order prover. In: Proc. of the, Description Logic Workshop (DL 2003), CEUR, vol. 81, pp. 152–159 (2003), http://ceur-ws.org/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tsarkov, D., Riazanov, A., Bechhofer, S., Horrocks, I. (2004). Using Vampire to Reason with OWL. In: McIlraith, S.A., Plexousakis, D., van Harmelen, F. (eds) The Semantic Web – ISWC 2004. ISWC 2004. Lecture Notes in Computer Science, vol 3298. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30475-3_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-30475-3_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23798-3
Online ISBN: 978-3-540-30475-3
eBook Packages: Springer Book Archive