Abstract
The Semantic Web vision is being realized to reach the full potential of the Web. Semantic data modeling is the foundation of the Semantic Web. The Web Ontology Language (OWL) and OWL Rules Language (ORL) provides basic machinery to the semantic mark-up for data. However, there is limited tool support for OWL and no tool support currently for ORL. In this paper, we propose to model OWL and ORL language semantics in PVS specification language so that OWL and ORL ontologies can be transformed and verified in the Prototype Verification System (PVS). PVS user-defined proof strategies are also developed to automate the proof process.
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.
References
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. 2174, pp. 396–408. Springer, Heidelberg (2001)
Berners-Lee, T., Hendler, J., Lassila, O.: The Semantic Web. Scientific American 284(5), 35–43 (2001)
Berners-Lee, T.: Notation 3 – Ideas about Web architecture (1998), http://www.w3.org/DesignIssues/Notation3.html
Brickley, D., Guha, R.V. (eds.): Resource description framework (rdf) schema specification 1.0 (February 2004), http://www.w3.org/TR/rdf-schema/
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)
Burstein, M., Hobbs, J., Lassila, O., Martin, D., McIlraith, S., Narayanan, S., Paolucci, M., Payne, T., Sycara, K., Zeng, H.: Daml service, http://www.daml.org/services/daml-s/2001/05/
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), http://www.w3.org/TR/owl-ref/
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–722 (May 2004)
Haarslev, V., Möller, 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)
Haarslev, V., Möller, R.: RACER User’s Guide and Reference Manual: Version 1.7.6 (December 2002)
Horrocks, I.: The faCT system. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 307–312. Springer, Heidelberg (1998)
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–731. ACM, New York (2004), http://www.cs.man.ac.uk/~horrocks/DAML/Rules/
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–733. ACM Press, New York (2000)
Manola, F., Miller, E. (eds.): RDF Primer (February 2004), http://www.w3.org/TR/rdf-primer/
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–40. Cambridge University Press, Cambridge (2003)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
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)
Saaltink, M.: The Z/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–85. Springer, Heidelberg (1997)
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)
Wang, H.: Semantic Web and Formal Design Methods. PhD thesis, National University of Singapore (2004)
World Wide Web Consortium (W3C). OWL Web Ontology Language Overview (March 2003), http://www.w3.org/TR/owl-features/
World Wide Web Consortium (W3C). Web Ontology Language (OWL) Use Cases and Requirements (March 2003), http://www.w3.org/TR/webont-req/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dong, J.S., Feng, Y., Li, Y.F. (2005). Verifying OWL and ORL Ontologies in PVS. In: Liu, Z., Araki, K. (eds) Theoretical Aspects of Computing - ICTAC 2004. ICTAC 2004. Lecture Notes in Computer Science, vol 3407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31862-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-31862-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25304-4
Online ISBN: 978-3-540-31862-0
eBook Packages: Computer ScienceComputer Science (R0)