{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:18:29Z","timestamp":1725549509459},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253044"},{"type":"electronic","value":"9783540318620"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31862-0_20","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:28:55Z","timestamp":1268400535000},"page":"265-279","source":"Crossref","is-referenced-by-count":1,"title":["Verifying OWL and ORL Ontologies in PVS"],"prefix":"10.1007","author":[{"given":"Jin Song","family":"Dong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuzhang","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan Fang","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","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)"},{"issue":"5","key":"20_CR2","doi-asserted-by":"publisher","first-page":"35","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), 35\u201343 (2001)","journal-title":"Scientific American"},{"key":"20_CR3","unstructured":"Berners-Lee, T.: Notation 3 \u2013 Ideas about Web architecture (1998), \n                    \n                      http:\/\/www.w3.org\/DesignIssues\/Notation3.html"},{"key":"20_CR4","unstructured":"Brickley, D., Guha, R.V. (eds.): Resource description framework (rdf) schema specification 1.0 (February 2004), \n                    \n                      http:\/\/www.w3.org\/TR\/rdf-schema\/"},{"key":"20_CR5","unstructured":"Broekstra, J., Klein, M., Decker, S., Fensel, D., Horrocks, I.: Adding formal semantics to the web: building on top of rdf schema. In: ECDL Workshop on the Semantic Web: Models, Architectures and Management (2000)"},{"key":"20_CR6","unstructured":"Burstein, M., Hobbs, J., Lassila, O., Martin, D., McIlraith, S., Narayanan, S., Paolucci, M., Payne, T., Sycara, K., Zeng, H.: Daml service, \n                    \n                      http:\/\/www.daml.org\/services\/daml-s\/2001\/05\/"},{"key":"20_CR7","unstructured":"Dean, M., Connolly, D., van Harmelen, F., Hendler, J., Horrocks, I., McGuinness, D.L., Patel-Schneider, P.F., Stein, L.A. (eds.): OWL Web Ontology Language 1.0 Reference (2002), \n                    \n                      http:\/\/www.w3.org\/TR\/owl-ref\/"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Dong, J.S., Lee, C.H., Li, Y.F., Wang, H.: A combined approach to checking web ontologies. In: Proceedings of 13th World Wide Web Conference (WWW 2004), New York, USA, pp. 714\u2013722 (May 2004)","DOI":"10.1145\/988672.988770"},{"key":"20_CR9","unstructured":"Haarslev, V., M\u00f6ller, R.: Practical Reasoning in Racer with a Concrete Domain for Linear Inequations. In: Horrocks, I., Tessaris, S. (eds.) Proceedings of the International Workshop on Description Logics (DL-2002), Toulouse, France, April 2002, CEUR-WS (2002)"},{"key":"20_CR10","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER User\u2019s Guide and Reference Manual: Version 1.7.6 (December 2002)"},{"key":"20_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/3-540-69778-0_30","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"I. Horrocks","year":"1998","unstructured":"Horrocks, I.: The faCT system. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 307\u2013312. Springer, Heidelberg (1998)"},{"key":"20_CR12","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), New York, USA, pp. 723\u2013731. ACM, New York (2004), \n                    \n                      http:\/\/www.cs.man.ac.uk\/~horrocks\/DAML\/Rules\/"},{"key":"20_CR13","first-page":"730","volume-title":"The 22nd International Conference on Software Engineering (ICSE 2000)","author":"D. Jackson","year":"2000","unstructured":"Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the Alloy Constraint Analyzer. In: The 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, June 2000, pp. 730\u2013733. ACM Press, New York (2000)"},{"key":"20_CR14","unstructured":"Manola, F., Miller, E. (eds.): RDF Primer (February 2004), \n                    \n                      http:\/\/www.w3.org\/TR\/rdf-primer\/"},{"key":"20_CR15","first-page":"1","volume-title":"The description logic handbook: theory, implementation, and applications","author":"D. Nardi","year":"2003","unstructured":"Nardi, D., Brachman, R.J.: An introduction to description logics. In: Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.) The description logic handbook: theory, implementation, and applications, pp. 1\u201340. Cambridge University Press, Cambridge (2003)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"20_CR17","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. Computer Science Laboratory, Menlo Park, CA. SRI International (December 2001)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 72\u201385. Springer, Heidelberg (1997)"},{"key":"20_CR19","unstructured":"van Harmelen, F., Patel-Schneider, P.F., Horrocks, I. (eds.): Reference description of the DAML+OIL ontology markup language. Contributors: Berners-Lee, T., Brickley, D., Connolly, D., Dean, M., Decker, S., Hayes, P., Heflin, J., Hendler, J., Lassila, O., McGuinness, D., Stein, L.A..., (March 2001)"},{"key":"20_CR20","unstructured":"Wang, H.: Semantic Web and Formal Design Methods. PhD thesis, National University of Singapore (2004)"},{"key":"20_CR21","unstructured":"World Wide Web Consortium (W3C). OWL Web Ontology Language Overview (March 2003), \n                    \n                      http:\/\/www.w3.org\/TR\/owl-features\/"},{"key":"20_CR22","unstructured":"World Wide Web Consortium (W3C). Web Ontology Language (OWL) Use Cases and Requirements (March 2003), \n                    \n                      http:\/\/www.w3.org\/TR\/webont-req\/"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31862-0_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:29:59Z","timestamp":1605760199000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31862-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253044","9783540318620"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31862-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}