{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T18:43:59Z","timestamp":1791312239072,"version":"4.3.1"},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540317821","type":"print"},{"value":"9783540317845","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11663881_12","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T11:31:46Z","timestamp":1137670306000},"page":"201-218","source":"Crossref","is-referenced-by-count":18,"title":["Reasoning Support for Expressive Ontology Languages Using a Theorem Prover"],"prefix":"10.1007","author":[{"given":"Ian","family":"Horrocks","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning, ch. 2","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2, vol.\u00a0I, pp. 19\u201399. Elsevier Science, Amsterdam (2001)"},{"key":"12_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-45422-5_28","volume-title":"KI 2001: Advances in Artificial Intelligence","author":"S. Bechhofer","year":"2001","unstructured":"Bechhofer, S., Horrocks, I., Goble, C., Stevens, R.: OilEd: A reason-able ontology editor for the semantic web. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001. LNCS (LNAI), vol.\u00a02174, pp. 396\u2013408. Springer, Heidelberg (2001)"},{"key":"12_CR3","unstructured":"Bechhofer, S., van Harmelen, F., Hendler, J., Horrocks, I., McGuinness, D.L., Patel-Schneider, P.F., Stein, L.A.: OWL web ontology language 1.0 reference. W3C Recommendation, February 10 (2004), Available at http:\/\/www.w3.org\/TR\/owl-ref\/"},{"key":"12_CR4","unstructured":"Berardi, D., Gr\u00fcninger, M., Hull, R., McIlraith, S.: Towards a first-order ontology for semantic web services (September 2004), http:\/\/www.w3.org\/2004\/08\/ws-cc\/mci-20040904"},{"issue":"5","key":"12_CR5","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1038\/scientificamerican0501-34","volume":"284","author":"T. Berners-Lee","year":"2001","unstructured":"Berners-Lee, T., Hendler, J., Lassila, O.: The semantic Web. Scientific American\u00a0284(5), 34\u201343 (2001)","journal-title":"Scientific American"},{"key":"12_CR6","unstructured":"Boley, H., Dean, M., Grosof, B., Sintek, M., Spencer, B., Tabet, S., Wagner, G.: First-Order-Logic RuleML (2004), http:\/\/www.ruleml.org\/fol\/"},{"key":"12_CR7","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve mace-style model finding. In: Proceedings of the Workshop Model Computation 2003 (2003)"},{"issue":"1-2","key":"12_CR8","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0747-7171(03)00036-1","volume":"36","author":"A. Degtyarev","year":"2003","unstructured":"Degtyarev, A., Nieuwenhuis, R., Voronkov, A.: Stratified resolution. Journal of Symbolic Computations\u00a036(1-2), 79\u201399 (2003)","journal-title":"Journal of Symbolic Computations"},{"key":"12_CR9","unstructured":"Emmen, A.: The grid needs ontologies\u2014onto-what? (2002), http:\/\/www.hoise.com\/primeur\/03\/articles\/monthly\/AE-PR-02-03-7.html"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Fikes, R., Hayes, P., Horrocks, I.: OWL-QL\u2014a language for deductive query answering on the Semantic Web. Journal of Web Semantics (2004) (to appear)","DOI":"10.1016\/j.websem.2004.07.002"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Foster, I., Kesselman, C., Nick, J., Tuecke, S.: The physiology of the grid: An open grid services architecture for distributed systems integration (2002), http:\/\/www.globus.org\/research\/papers\/ogsa.pdf","DOI":"10.1109\/MC.2002.1009167"},{"key":"12_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-45085-6_31","volume-title":"Automated Deduction \u2013 CADE-19","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 335\u2013349. Springer, Heidelberg (2003)"},{"key":"12_CR13","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER User\u2019s Guide and Reference Manual. Version 1.7.7 (September 2003)"},{"key":"12_CR14","unstructured":"Hayes, P., Menzel, C.: A semantics for the knowledge interchange format. In: IJCAI 2001 Workshop on the IEEE Standard Upper Ontology (2001)"},{"key":"12_CR15","first-page":"636","volume-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR 1998)","author":"I. Horrocks","year":"1998","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Cohn, A., Schubert, L., Shapiro, S. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR 1998), pp. 636\u2013647. Morgan Kaufmann, San Francisco (1998)"},{"key":"12_CR16","unstructured":"Horrocks, I., Li, L., Turi, D., Bechhofer, S.: The instance store: DL reasoning with large numbers of individuals. In: Proc. of the 2004 Description Logic Workshop (DL 2004), pp. 31\u201340 (2004)"},{"key":"12_CR17","first-page":"723","volume-title":"Proc. of the Thirteenth International World Wide Web Conference (WWW 2004)","author":"I. Horrocks","year":"2004","unstructured":"Horrocks, I., Patel-Schneider, P.F.: A proposal for an OWL rules language. In: Proc. of the Thirteenth International World Wide Web Conference (WWW 2004), pp. 723\u2013731. ACM, New York (2004)"},{"key":"12_CR18","unstructured":"Horrocks, I., Patel-Schneider, P.F., Boley, H., Tabet, S., Grosof, B., Dean, M.: SWRL: A semantic web rule language combining owl and ruleml. W3C Note, May 21 (2004), Available at http:\/\/www.w3.org\/Submission\/SWRL\/"},{"key":"12_CR19","first-page":"792","volume-title":"Proc. of the 18th National Conference on Artificial Intelligence (AAAI 2002)","author":"I. Horrocks","year":"2002","unstructured":"Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: 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), pp. 792\u2013797. AAAI Press, Menlo Park (2002)"},{"issue":"1","key":"12_CR20","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/j.websem.2003.07.001","volume":"1","author":"I. Horrocks","year":"2003","unstructured":"Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From SHIQ and RDF to OWL: The making of a web ontology language. Journal of Web Semantics\u00a01(1), 7\u201326 (2003)","journal-title":"Journal of Web Semantics"},{"key":"12_CR21","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, San Francisco (2003)"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/3-540-48005-6_15","volume-title":"The Semantic Web - ISWC 2002","author":"I. Horrocks","year":"2002","unstructured":"Horrocks, I., Tessaris, S.: Querying the semantic web: a formal approach. In: Horrocks, I., Hendler, J. (eds.) ISWC 2002. LNCS, vol.\u00a02342, pp. 177\u2013191. Springer, Heidelberg (2002)"},{"key":"12_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-25984-8_23","volume-title":"Automated Reasoning","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Konev, B., Riazanov, A., Voronkov, A.: TeMP: A temporal monodic prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 326\u2013330. Springer, Heidelberg (2004)"},{"key":"12_CR24","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"SAT 2000: Highlights of Satisfiability Research in the Year 2000","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: Using resolution for testing modal satisfiability and building models. In: Gent, I.P., van Maaren, H., Walsh, T. (eds.) SAT 2000: Highlights of Satisfiability Research in the Year 2000. Frontiers in Artificial Intelligence and Applications, vol.\u00a063. IOS Press, Amsterdam (2000); Also to appear in a special issue of Journal of Automated Reasoning"},{"key":"12_CR25","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/775152.775159","volume-title":"Proceedings of the Twelfth International World Wide Web Conference, WWW 2003","author":"P.P.-S.I. Horrocks","year":"2003","unstructured":"Horrocks, P.P.-S.I.: Three theses of representation in the semantic web. In: Proceedings of the Twelfth International World Wide Web Conference, WWW 2003, Budapest, Hungary, pp. 39\u201347. ACM, New York (2003)"},{"key":"12_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-36078-6_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T. Kutsia","year":"2002","unstructured":"Kutsia, T.: Theorem proving with sequence variables and flexible arity symbols. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 278\u2013291. Springer, Heidelberg (2002)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide. Technical Memorandum 264, Argonne National Laboratory (August. 2003)","DOI":"10.2172\/822574"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 3.3 reference manual. Technical Memorandum 263, Argonne National Laboratory (August 2003)","DOI":"10.2172\/822573"},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1145\/988672.988748","volume-title":"WWW 2004, Proceedings of the 13th international conference on World Wide Web","author":"P. Mika","year":"2004","unstructured":"Mika, P., Oberle, D., Gangemi, A., Sabou, M.: Foundations for service ontologies: Aligning OWL-S dolce. In: Feldman, S., Uretsky, M., Najork, M., Wills, C. (eds.) WWW 2004, Proceedings of the 13th international conference on World Wide Web, pp. 563\u2013572. ACM, New York (2004)"},{"key":"12_CR30","unstructured":"Pease, A., Niles, I., Li, J.: 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)"},{"key":"12_CR31","unstructured":"Prot\u00e9g\u00e9 (2003), http:\/\/protege.stanford.edu\/"},{"key":"12_CR32","unstructured":"Rector, A.: Analysis of propagation along transitive roles: Formalisation of the galen experience with medical ontologies. In: Proc. of DL 2002. CEUR (2002), http:\/\/ceur-ws.org\/"},{"key":"12_CR33","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0933-3657(96)00369-7","volume":"9","author":"A. Rector","year":"1997","unstructured":"Rector, A., Bechhofer, S., Goble, C.A., Horrocks, I., Nowlan, W.A., Solomon, W.D.: The Grail concept modelling language for medical terminology. Artificial Intelligence in Medicine\u00a09, 139\u2013171 (1997)","journal-title":"Artificial Intelligence in Medicine"},{"key":"12_CR34","unstructured":"Rector, A., Horrocks, I.: 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 1997 (1997)"},{"issue":"2-3","key":"12_CR35","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"},{"issue":"1-2","key":"12_CR36","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A. Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. Journal of Symbolic Computations\u00a036(1-2), 101\u2013115 (2003)","journal-title":"Journal of Symbolic Computations"},{"key":"12_CR37","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/3-540-48229-6_41","volume-title":"Artificial Intelligence in Medicine","author":"S. Schulz","year":"2001","unstructured":"Schulz, S., Hahn, U.: Parts, locations, and holes - formal reasoning about anatomical structures. In: Quaglini, S., Barahona, P., Andreassen, S. (eds.) AIME 2001. LNCS (LNAI), vol.\u00a02101, p. 293. Springer, Heidelberg (2001)"},{"key":"12_CR38","unstructured":"Common Logic Standard, http:\/\/cl.tamu.edu\/"},{"key":"12_CR39","doi-asserted-by":"publisher","first-page":"1853","DOI":"10.1016\/B978-044450813-3\/50028-X","volume-title":"Handbook of Automated Reasoning, ch. 26","author":"R. Sekar","year":"2001","unstructured":"Sekar, R., Ramakrishnan, I., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 26, vol.\u00a0II, pp. 1853\u20131964. Elsevier Science, Amsterdam (2001)"},{"key":"12_CR40","unstructured":"Spackman, K.: 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)"},{"issue":"2","key":"12_CR41","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1109\/TITB.2002.1006301","volume":"6","author":"R. Stevens","year":"2002","unstructured":"Stevens, R., Goble, C., Horrocks, I., Bechhofer, S.: Building a bioinformatics ontology using OIL. IEEE Transactions on Information Technology in Biomedicine\u00a06(2), 135\u2013141 (2002)","journal-title":"IEEE Transactions on Information Technology in Biomedicine"},{"issue":"4","key":"12_CR42","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1093\/logcom\/5.4.449","volume":"5","author":"T. Tammet","year":"1995","unstructured":"Tammet, T.: Completeness of resolution for definite answers. Journal of Logic and Computation\u00a05(4), 449\u2013471 (1995)","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"12_CR43","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":"12_CR44","unstructured":"The DAML Services Coalition. DAML-S: Web service description for the semantic web. In: ISWC 2003. LNCS, vol.\u00a02870. Springer, Heidelberg (2003)"},{"key":"12_CR45","volume-title":"Semantic Web 2004","author":"D. Tsarkov","year":"2004","unstructured":"Tsarkov, D., Riazanov, A., Bechhofer, S., Horrocks, I.: Using Vampire to reason with OWL. In: Semantic Web 2004. Springer, Heidelberg (2004) (to appear)"},{"key":"12_CR46","unstructured":"Tuecke, S., Czajkowski, K., Foster, I., Frey, J., Graham, S., Kesselman, C., Vanderbilt, P.: Grid service specification (draft). GWD-I draft, GGF Open Grid Services Infrastructure Working Group (2002)"},{"key":"12_CR47","doi-asserted-by":"crossref","unstructured":"Uschold, M., King, M., Moralee, S., Zorgios, Y.: The enterprise ontology. Knowledge Engineering Review\u00a013 (1998)","DOI":"10.1017\/S0269888998001088"},{"key":"12_CR48","unstructured":"van Harmelen, F., Patel-Schneider, P.F., Horrocks, I.: Reference description of the DAML+OIL, ontology markup langauge (March 2001)"},{"key":"12_CR49","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/3-540-48660-7_35","volume-title":"Automated Deduction - CADE-16","author":"A. Voronkov","year":"1999","unstructured":"Voronkov, A.: $k\\rotatebox[]{180}{K}$ : a theorem prover for K. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 383\u2013387. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Information and Knowledge Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11663881_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:04:30Z","timestamp":1605643470000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11663881_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540317821","9783540317845"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/11663881_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}