Abstract
While context is crucial for reasoning about ontologies as well as for conceptual modeling, its formal definition is often imprecise and its implementation in standard classical logic-based theories suffers from a lack of expressiveness and leads to ambiguities. In this chapter, it is shown that a two-layered language using the Calculus of Inductive Constructions (i.e., the Coq language) as a lower layer, and an ontological upper layer for giving types their meaning is able to support a clear and expressive semantics for context specification.
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
Notes
- 1.
The symbol “\(:\)” refers here to an assertion.
- 2.
Hierarchies using the part-whole relation.
- 3.
All their proper parts are present at any time they are present, such as a person.
- 4.
Entities that happen in time, and can have temporal parts such as a discussion.
- 5.
Automated sequence transforming a typed expression.
- 6.
The instantiation relation (:) and the subsumption (\texttt{:>} in Structure) are already available in the Coq language and do not require any supplementary modeling structures.
References
Agostini, A., et al.: Experience report: ontological reasoning for context-aware internet services. Paper presented at the 4th IEEE conference on pervasive computing and communications workshops (PerCom 2006 Workshops), IEEE Computer Society, Pisa, Italy, 13–17 March 2006
Barlatier, P., Dapoigny, R.: A type-theoretical approach for ontologies: The case of roles. Appl. Ontol. 7(3), 311–356 (2012). doi:10.3233/AO-2012-0113
Benerecetti, M., et al.: Contextual reasoning distilled. J. Exp. Theo. Artif. Intell. 12(3), 279–305 (2000)
Bertot, Y., Castéran, P.: Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science, An EATCS Series. Springer, Berlin (2004)
Bettini, C., et al.: A survey of context modelling and reasoning techniques. J. Pervasive Mobile Comput. 6(2), 161–180 (2010) (Elsevier Science Publishers B. V.)
Cohn, A.G., et al.: Qualitative spatial representation and reasoning with the region connection calculus. GeoInformatica 1, 275–316 (1997)
Dapoigny, R., Barlatier, P.: Modeling contexts with dependent types. Fundamenta Informaticae 104(4), 293–327 (2010). doi:10.3233/FI-2010-351
Dapoigny, R., Barlatier, P.: Formal foundations for situation awareness based on dependent type theory. Inf. Fus. 14(1), 87–107 (2013a). doi:10.1016/j.inffus.2012.02.006
Dapoigny, R., Barlatier, P.: Modeling ontological structures with type classes in Coq. Paper presented at the 20th international conference on conceptual structures (ICCS'2013), Lecture Notes in Computer Science, vol. 7735, pp. 135–152. Mumbai, India, 10–12 January 2013b
Gangemi, A., et al.: Sweetening ontologies with DOLCE. In: Gomez-Perez, A., Benjamins, V.R. (eds.) Paper presented at the 13th international conference EKAW'2002, Lecture Notes in Computer Science, vol. 2473, pp. 166–181. Siguenza, Spain, 1–4 Oct 2002
Ghidini, C., Giunchiglia, F.: Local models semantics, or contextual reasoning = locality + compatibility. Artif. Intell. 127(2), 221–259 (2001). doi:10.1016/S0004-3702(01)00064-9
Gonzalez, A.J., et al.: Formalizing context-based reasoning: a modeling paradigm for representing tactical human behavior. Int. J. Intell. Syst. 23, 822–847 (2008). doi:10.1002/int.20291
Grau, B.C., et al.: Modularity and web ontologies. Paper presented at the 10th international conference on principles of knowledge representation and reasoning, Lake District, United Kingdom, pp. 198–209, 2–5 July 2006
Guizzardi, G.: On ontology, ontologies, conceptualizations, modeling languages, and (meta)models. Paper presented at the 7th international Baltic conference, DB&IS 2006, Vilnius, Lithuania, 3–6 July 2006. Frontiers in Artificial Intelligence and Applications, vol. 155, pp. 18–39. IOS Press (2006)
Guizzardi, G., et al.: Towards ontological foundations for UML conceptual models. Paper presented at the confederated international conferences DOA, CoopIS and ODBASE'2002 Irvine, California, USA, 30 Oct–1 Nov 2002. Lecture Notes in Computer Science, vol. 2519, pp. 1100–1117 (2002)
Henricksen, K., Indulska, J.: Developing context-aware pervasive computing applications: models and approach. Pervasive Mobile Comput. 2(1), 37–64 (2006)
Krummenacher, R., Strang, T.: Ontology-based context modeling. Paper presented at the 3rd workshop on context-aware proactive systems, University of Surrey, United Kingdom, 18–19 June 2007
Loke, S.W.: Logic programming for context-aware pervasive computing: Language support, characterizing situations, and integration with the web. Paper presented at the IEEE/WIC/ACM international conference on web intelligence, Beijing, China, pp. 44–50, 20–24 Sept 2004
McCarthy, J.: Notes on formalizing context. Paper presented at the 13th international joint conference on artificial intelligence, Chambéry, France, pp. 555–560, 28 Aug–3 Sept 1993
Noonan, H.: Identity. The Stanford Encyclopedia of Philosophy. In: Edward, N.Z. (ed.). http://plato.stanford.edu/archives/win2011/entries/identity/ (2011). Accessed 7 Nov 2009
Perttunen, M., et al.: Context representation and reasoning in pervasive computing: a review. Int. J. Multimed. Ubiquit. Eng. 4(4), 1–28 (2009)
Pires, L.F., et al.: Techniques for describing and manipulating context information. Lucent Technologies, Freeband/A_MUSE, Tech. report D3.5v2.0 (2005)
Ranganathan, A., Campbell, R.H.: An infrastructure for context-awareness based on first order logic. Pers. Ubiquit. Comput. 7(6), 353–364 (2003) (Springer)
Schmidtke, H.R.: Aggregations and constituents: geometric specification of multi-granular objects. J. Vis. Lang. Comput. 16, 289–309 (2005) (Elsevier)
Schmidtke, H.R.: Contextual reasoning in context-aware systems. Paper presented at the 8th international conference on intelligent environments, Guanajuato, Mexico, pp. 82–93, 27–28 June 2012
Sowa, J.F.: Using a lexicon of canonical graphs in a semantic interpreter. In: Evens, M. (ed.) Relational Models of the Lexicon, pp. 113–137. Cambridge University Press, New York (1988)
Sozeau, M., Oury, N.: First-class type classes. In: Aït Mohamed, O., Mu˜noz, C., Tahar, S. (eds.) Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science, vol. 5170, pp. 278–293. Springer, Berlin (2008)
Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795–825 (2011). doi:10.1017/S0960129511000119
Studer, R., et al.: Knowledge engineering: principles and methods. Data Knowl. Eng. 25(1/2), 161–197 (1998)
Wang, X.H., et al.: Ontology-based context modeling and reasoning using OWL. Paper presented at the 2nd IEEE conference on pervasive computing and communications (PerCom 2004), Orlando, Florida, 14–17 March 2004. Workshop on context modeling and reasoning CoMoRea'04, pp. 18–22. IEEE Press, USA (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer Science+Business Media New York
About this chapter
Cite this chapter
Dapoigny, R., Barlatier, P. (2014). Formalizing Context for Domain Ontologies in Coq. In: Brézillon, P., Gonzalez, A. (eds) Context in Computing. Springer, New York, NY. https://doi.org/10.1007/978-1-4939-1887-4_27
Download citation
DOI: https://doi.org/10.1007/978-1-4939-1887-4_27
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4939-1886-7
Online ISBN: 978-1-4939-1887-4
eBook Packages: Computer ScienceComputer Science (R0)