Abstract
In the domain of ontology design as well as in Conceptual Modeling, representing part-whole relations is a long-standing challenging problem. However, in most papers the focus has been on properties of the part-whole relation, rather than on its semantics. In the last decades, most approaches which have addressed the formal specification of the part-whole relation (i) rely on First Order Logic (FOL) which is unable to address multiple levels of granularity and (ii) do not support any typing mechanism useful for the extensional side of concepts and then, many difficulties remain especially about expressiveness. In mathematical logic and program checking, type theories have proved to be appealing but so far, they have not been applied in the formalization of ontological relations. To bridge this gap, we present an axiomatization of the part-whole relation which hold between typed terms. Relation structures in the dependently-typed framework rely on a constructive logic. We define in a precise way what relation structures and their meta-properties, are in term of type classes using the Coq language.
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.
Similar content being viewed by others
References
Guarino, N., Welty, C.: A Formal Ontology of Properties. In: Dieng, R., Corby, O. (eds.) EKAW 2000. LNCS (LNAI), vol. 1937, pp. 97–112. Springer, Heidelberg (2000)
Smith, B., Rosse, C.: The Role of Foundational Relations in the Alignment of Biomedical Ontologies. In: Fieschi, M., et al. (eds.) MEDINFO 2004, pp. 444–448. IOS Press, Amsterdam (2004)
Guizzardi, G., Wagner, G.: What’s in a Relationship: An Ontological Analysis. In: Li, Q., Spaccapietra, S., Yu, E., Olivé, A. (eds.) ER 2008. LNCS, vol. 5231, pp. 83–97. Springer, Heidelberg (2008)
Artale, A., Franconi, E., Guarino, N., Pazzi, L.: Part-whole relations in object-centered systems: An overview. Data and Knowledge Engineering 20(3), 347–383 (1996)
Bittner, T., Smith, B.: A Theory of Granular Partitions. In: Duckham, M., Goodchild, M.F., Worboys, M. (eds.) Foundations of Geographic Information Science, vol. 7, pp. 124–125 (2003)
Schwarz, U., Smith, B.: Ontological Relations. In: Munn, K., Smith, B. (eds.) Applied Ontology: An Introduction, Ch. 10, pp. 219–234. Ontos Verlag (2008)
Keet, C.M., Artale, A.: Representing and reasoning over a taxonomy of part-whole relations. Applied Ontology 3(1-2), 91–110 (2008)
Dapoigny, R., Barlatier, P.: Towards Ontological Correctness of Part-whole Relations with Dependent Types. In: Procs. of the Sixth Int. Conference (FOIS 2010), pp. 45–58 (2010)
Simons, P.: Parts: A Study in Ontology. Clarendon Press, Oxford (1987)
Varzi, A.C.: Parts, wholes, and part-whole relations: The prospects of mereotopology. Data and Knowledge Engineering 20(3), 259–286 (1996)
Johansson, I.: On the transitivity of the parthood relations. In: Hochberg, H., Mulligan, K. (eds.) Relations and Predicates, pp. 161–181. Ontos Verlag (2004)
Lewis, D.: Parts of Classes, pp. 79–93. Blackwell Publishers, Oxford (1991)
Opdahl, A.L., Henderson-Sellers, B., Barbier, F.: Ontological analysis of whole-part relationships in OO-models. Information and Software Technology 43, 387–399 (2001)
Aitken, J.S., Webber, B.L., Bard, J.B.: Part-of relations in anatomy ontologies: A proposal for RDFS and OWL formalisations. In: Procs. of the Pacific Symp. on Biocomputing, pp. 6–10 (2004)
Schulz, S., Stenzhorn, H., Boeker, M., Smith, B.: Strengths and limitations of formal ontologies in the biomedical domain. Elec. J. of Com., Inf. and Innovation in Health 3(1), 31–45 (2009)
Guizzardi, G.: On the Representation of Quantities and their Parts in Conceptual Modeling. In: Procs. of the Sixth Int. Conference (FOIS 2010), pp. 103–116. IOS Press (2010)
Gerstl, P., Pribbenow, S.: Midwinters, End Games, and Body Parts: a Classification of Part-whole Relations. Int. Journal of Human-Computer Studies 43, 865–889 (1995)
Angelov, K., Enache, R.: Typeful Ontologies with Direct Multilingual Verbalization. In: Rosner, M., Fuchs, N.E. (eds.) CNL 2010. LNCS, vol. 7175, pp. 1–20. Springer, Heidelberg (2012)
Cirstea, H., Coquery, E., Drabent, W., Fages, F., Kirchner, C., Maluszynski, J., Wack, B.: Types for Web Rule Languages: a preliminary study, technical report A04-R-560, PROTHEO - INRIA Lorraine - LORIA (2004)
Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. Journal of Functional Programming 14(1), 3–19 (2004)
Bertot, Y., Théry, L.: Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 173–181. Springer, Heidelberg (2008)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. An EATCS series. Springer (2004)
Dapoigny, R., Barlatier, P.: Modeling Ontological Structures with Type Classes in Coq. In: Pfeiffer, H.D., Ignatov, D.I., Poelmans, J., Gadiraju, N. (eds.) ICCS 2013. LNCS, vol. 7735, pp. 135–152. Springer, Heidelberg (2013)
Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21(4), 795–825 (2011)
Sowa, J.F.: Using a lexicon of canonical graphs in a semantic interpreter. In: Relational Models of the Lexicon, pp. 113–137. Cambridge University Press (1988)
Masolo, C., Borgo, S., Gangemi, A., Guarino, N., Oltramari, A.: Ontology Library (D18), Laboratory for Applied Ontology-ISTC-CNR (2003)
Gangemi, A., Guarino, N., Masolo, C., Oltramari, A., Schneider, L.: Sweetening ontologies with DOLCE. In: Gómez-Pérez, A., Benjamins, V.R. (eds.) EKAW 2002. LNCS (LNAI), vol. 2473, pp. 166–181. Springer, Heidelberg (2002)
Smith, B.: Mereotopology: A Theory of Parts and Boundaries. Data and Knowledge Engineering 20, 287–303 (1996)
Varzi, A.C.: Mereology. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2012), http://plato.stanford.edu/archives/win2012/entries/mereology
Kumar, A., Smith, B., Novotny, D.: Biomedical Informatics and granularity. Comparative and Functional Genomics 5(6-7), 501–508 (2004)
Rector, A., Rogers, J., Bittner, T.: Granularity, scale and collectivity: When size does and does not matter. J. of Biomedical Informatics 39(3), 333–349 (2006)
Donnelly, M., Bittner, T., Rosse, C.: A formal theory for spatial representation and reasoning in biomedical ontologies. Artificial Intelligence in Medicine 36(1), 1–27 (2005)
Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning 2(1), 41–62 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Dapoigny, R., Barlatier, P. (2014). Specifying Well-Formed Part-Whole Relations in Coq. In: Hernandez, N., Jäschke, R., Croitoru, M. (eds) Graph-Based Representation and Reasoning. ICCS 2014. Lecture Notes in Computer Science(), vol 8577. Springer, Cham. https://doi.org/10.1007/978-3-319-08389-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-08389-6_14
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08388-9
Online ISBN: 978-3-319-08389-6
eBook Packages: Computer ScienceComputer Science (R0)