{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:49Z","timestamp":1761611269441},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237983"},{"type":"electronic","value":"9783540304753"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30475-3_33","type":"book-chapter","created":{"date-parts":[[2010,9,23]],"date-time":"2010-09-23T21:22:54Z","timestamp":1285276974000},"page":"471-485","source":"Crossref","is-referenced-by-count":28,"title":["Using Vampire to Reason with OWL"],"prefix":"10.1007","author":[{"given":"Dmitry","family":"Tsarkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Riazanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sean","family":"Bechhofer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Horrocks","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"volume-title":"The Description Logic Handbook: Theory, Implementation and Applications","year":"2002","key":"33_CR1","unstructured":"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)"},{"key":"33_CR2","first-page":"270","volume-title":"Proc. of the 3rd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 1992)","author":"F. Baader","year":"1992","unstructured":"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\u2013281. Morgan Kaufmann, Los Altos (1992)"},{"key":"33_CR3","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: ResolutionTheorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 2, pp. 19\u201399. Elsevier Science, Amsterdam (2001)"},{"key":"33_CR4","first-page":"25","volume-title":"Proceedings of the Sixth International Conference on Intelligent Systems for Molecular Biology, ISMB 1998","author":"P.G. Baker","year":"1998","unstructured":"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\u201334. AAAI Press, Menlo Park (1998)"},{"key":"33_CR5","unstructured":"Biron, P.V., Malhotra, A.: XML schema part 2: Datatypes. W3C Recommendation (May 2001), \n                    \n                      http:\/\/www.w3.org\/TR\/xmlschema-2\/"},{"issue":"1-2","key":"33_CR6","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0004-3702(96)00004-5","volume":"82","author":"A. Borgida","year":"1996","unstructured":"Borgida, A.: On the relative expressiveness of description logics and predicate logics. Artificial Intelligence\u00a082(1-2), 353\u2013367 (1996)","journal-title":"Artificial Intelligence"},{"key":"33_CR7","unstructured":"The CASC web page, \n                    \n                      http:\/\/www.cs.miami.edu\/~tptp\/CASC\/"},{"key":"33_CR8","unstructured":"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), \n                    \n                      http:\/\/www.w3.org\/TR\/owl-ref\/"},{"key":"33_CR9","unstructured":"DL 1998 test suite, \n                    \n                      http:\/\/dl.kr.org\/dl98\/comparison\/"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013304 (1999)","DOI":"10.1109\/LICS.1999.782624"},{"key":"33_CR11","unstructured":"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), \n                    \n                      http:\/\/logic.stanford.edu\/kif\/Hypertext\/kif-manual.html"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Gradel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proceedings of LICS 1997, pp. 306\u2013317 (1997)","DOI":"10.1109\/LICS.1997.614957"},{"key":"33_CR13","unstructured":"Horrocks, I., Patel-Schneider, P.F., Boley, H., Tabet, S., Grosof, B., Dean, M.: SWRL: A SemanticWeb Rule Language Combining OWL and RuleML (2003), \n                    \n                      http:\/\/www.daml.org\/2003\/11\/swrl\/"},{"key":"33_CR14","unstructured":"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\u2013296 (2000)"},{"key":"33_CR15","unstructured":"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\u2013647 (1998)"},{"key":"33_CR16","unstructured":"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\u201335 (2001), \n                    \n                      http:\/\/ceur-ws.org\/Vol-49\/"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-39718-2_2","volume-title":"The Semantic Web - ISWC 2003","author":"I. Horrocks","year":"2003","unstructured":"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.\u00a02870, pp. 17\u201329. Springer, Heidelberg (2003)"},{"key":"33_CR18","unstructured":"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\u2013204 (2001)"},{"key":"33_CR19","first-page":"343","volume-title":"Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003)","author":"I. Horrocks","year":"2003","unstructured":"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\u2013348. Morgan Kaufmann, Los Altos (2003)"},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/10722086_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: MSPASS: Modal reasoning by translation and first-order resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol.\u00a01847, pp. 67\u201371. Springer, Heidelberg (2000)"},{"key":"33_CR21","unstructured":"Levy, A.Y., Rousset, M.-C.: CARIN: A representation language combining horn rules and description logics. In: European Conference on Artificial Intelligence, pp. 323\u2013327 (1996)"},{"key":"33_CR22","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1002\/malq.19750210118","volume":"21","author":"M. Mortimer","year":"1975","unstructured":"Mortimer, M.: On languages with two variables. Zeitschr. f\u00fcr math. Logik und Grundlagen der Math.\u00a021, 135\u2013140 (1975)","journal-title":"Zeitschr. f\u00fcr math. Logik und Grundlagen der Math."},{"issue":"2","key":"33_CR23","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"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\u00a018(2), 237\u2013246 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR24","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch.7, pp. 371\u2013443. Elsevier Science, Amsterdam (2001)"},{"key":"33_CR25","unstructured":"OWL test suite, \n                    \n                      http:\/\/www.w3.org\/TR\/owl-test\/"},{"issue":"3","key":"33_CR26","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1023\/A:1005866922570","volume":"20","author":"M. Paramasivam","year":"1998","unstructured":"Paramasivam, M., Plaisted, D.A.: Automated deduction techniques for classification in description logic systems. J. of Automated Reasoning\u00a020(3), 337\u2013364 (1998)","journal-title":"J. of Automated Reasoning"},{"key":"33_CR27","unstructured":"Patel-Schneider, P.F., Hayes, P., Horrocks, I.: OWL web ontology language semantics and abstract syntax. W3C Recommendation, February 10 (2004), Available at \n                    \n                      http:\/\/www.w3.org\/TR\/owl-semantics\/"},{"key":"33_CR28","unstructured":"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\u201993), Washington DC, USA, pp. 414\u2013418 (1993)"},{"issue":"2-3","key":"33_CR29","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"33_CR30","unstructured":"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\u2013471 (1991)"},{"key":"33_CR31","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library. TPTP v. 2.4.1. Technical report, University of Miami (2001)"},{"key":"33_CR32","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library. TPTP v. 2.4.1. Technical report, University of Miami (2001)"},{"issue":"2","key":"33_CR33","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. Journal of Automated Reasoning\u00a018(2), 199\u2013204 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR34","unstructured":"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), \n                    \n                      http:\/\/km.aifb.uni-karlsruhe.de\/ws\/psss03\/proceedings"},{"key":"33_CR35","unstructured":"Tobies, S.: Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, LuFG Theoretical Computer Science, RWTH-Aachen, Germany (2001)"},{"key":"33_CR36","unstructured":"Tsarkov, D., Horrocks, I.: DL reasoner vs. first-order prover. In: Proc. of the, Description Logic Workshop (DL 2003), CEUR, vol.\u00a081, pp. 152\u2013159 (2003), \n                    \n                      http:\/\/ceur-ws.org\/"}],"container-title":["Lecture Notes in Computer Science","The Semantic Web \u2013 ISWC 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30475-3_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T04:23:07Z","timestamp":1553142187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30475-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237983","9783540304753"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30475-3_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}