Specifying Well-Formed Part-Whole Relations in Coq

  • Richard DapoignyEmail author
  • Patrick Barlatier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8577)


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.


Type Theory Type Class Domain Ontology Dependent Type Proof Search 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefzbMATHGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Schwarz, U., Smith, B.: Ontological Relations. In: Munn, K., Smith, B. (eds.) Applied Ontology: An Introduction, Ch. 10, pp. 219–234. Ontos Verlag (2008)Google Scholar
  7. 7.
    Keet, C.M., Artale, A.: Representing and reasoning over a taxonomy of part-whole relations. Applied Ontology 3(1-2), 91–110 (2008)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Simons, P.: Parts: A Study in Ontology. Clarendon Press, Oxford (1987)Google Scholar
  10. 10.
    Varzi, A.C.: Parts, wholes, and part-whole relations: The prospects of mereotopology. Data and Knowledge Engineering 20(3), 259–286 (1996)CrossRefzbMATHGoogle Scholar
  11. 11.
    Johansson, I.: On the transitivity of the parthood relations. In: Hochberg, H., Mulligan, K. (eds.) Relations and Predicates, pp. 161–181. Ontos Verlag (2004)Google Scholar
  12. 12.
    Lewis, D.: Parts of Classes, pp. 79–93. Blackwell Publishers, Oxford (1991)zbMATHGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. Journal of Functional Programming 14(1), 3–19 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. An EATCS series. Springer (2004)Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    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)CrossRefGoogle Scholar
  25. 25.
    Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21(4), 795–825 (2011)CrossRefzbMATHMathSciNetGoogle Scholar
  26. 26.
    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)Google Scholar
  27. 27.
    Masolo, C., Borgo, S., Gangemi, A., Guarino, N., Oltramari, A.: Ontology Library (D18), Laboratory for Applied Ontology-ISTC-CNR (2003)Google Scholar
  28. 28.
    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)CrossRefGoogle Scholar
  29. 29.
    Smith, B.: Mereotopology: A Theory of Parts and Boundaries. Data and Knowledge Engineering 20, 287–303 (1996)CrossRefzbMATHGoogle Scholar
  30. 30.
    Varzi, A.C.: Mereology. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2012),
  31. 31.
    Kumar, A., Smith, B., Novotny, D.: Biomedical Informatics and granularity. Comparative and Functional Genomics 5(6-7), 501–508 (2004)CrossRefGoogle Scholar
  32. 32.
    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)CrossRefGoogle Scholar
  33. 33.
    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)CrossRefGoogle Scholar
  34. 34.
    Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning 2(1), 41–62 (2009)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  1. 1.LISTIC/Polytech’Annecy-ChambéryUniversity of SavoieAnnecy-le-vieux CedexFrance

Personalised recommendations