{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:38:41Z","timestamp":1742960321730,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319083889"},{"type":"electronic","value":"9783319083896"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08389-6_14","type":"book-chapter","created":{"date-parts":[[2014,7,17]],"date-time":"2014-07-17T10:43:39Z","timestamp":1405593819000},"page":"159-173","source":"Crossref","is-referenced-by-count":0,"title":["Specifying Well-Formed Part-Whole Relations in Coq"],"prefix":"10.1007","author":[{"given":"Richard","family":"Dapoigny","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Barlatier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-39967-4_8","volume-title":"Knowledge Engineering and Knowledge Management. Methods, Models, and Tools","author":"N. Guarino","year":"2000","unstructured":"Guarino, N., Welty, C.: A Formal Ontology of Properties. In: Dieng, R., Corby, O. (eds.) EKAW 2000. LNCS (LNAI), vol.\u00a01937, pp. 97\u2013112. Springer, Heidelberg (2000)"},{"key":"14_CR2","first-page":"444","volume-title":"MEDINFO 2004","author":"B. Smith","year":"2004","unstructured":"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\u2013448. IOS Press, Amsterdam (2004)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-87877-3_8","volume-title":"Conceptual Modeling - ER 2008","author":"G. Guizzardi","year":"2008","unstructured":"Guizzardi, G., Wagner, G.: What\u2019s in a Relationship: An Ontological Analysis. In: Li, Q., Spaccapietra, S., Yu, E., Oliv\u00e9, A. (eds.) ER 2008. LNCS, vol.\u00a05231, pp. 83\u201397. Springer, Heidelberg (2008)"},{"issue":"3","key":"14_CR4","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/S0169-023X(96)00013-4","volume":"20","author":"A. Artale","year":"1996","unstructured":"Artale, A., Franconi, E., Guarino, N., Pazzi, L.: Part-whole relations in object-centered systems: An overview. Data and Knowledge Engineering\u00a020(3), 347\u2013383 (1996)","journal-title":"Data and Knowledge Engineering"},{"doi-asserted-by":"crossref","unstructured":"Bittner, T., Smith, B.: A Theory of Granular Partitions. In: Duckham, M., Goodchild, M.F., Worboys, M. (eds.) Foundations of Geographic Information Science, vol.\u00a07, pp. 124\u2013125 (2003)","key":"14_CR5","DOI":"10.1201\/9780203009543.ch7"},{"doi-asserted-by":"crossref","unstructured":"Schwarz, U., Smith, B.: Ontological Relations. In: Munn, K., Smith, B. (eds.) Applied Ontology: An Introduction, Ch. 10, pp. 219\u2013234. Ontos Verlag (2008)","key":"14_CR6","DOI":"10.1515\/9783110324860.219"},{"issue":"1-2","key":"14_CR7","doi-asserted-by":"crossref","first-page":"91","DOI":"10.3233\/AO-2008-0044","volume":"3","author":"C.M. Keet","year":"2008","unstructured":"Keet, C.M., Artale, A.: Representing and reasoning over a taxonomy of part-whole relations. Applied Ontology\u00a03(1-2), 91\u2013110 (2008)","journal-title":"Applied Ontology"},{"unstructured":"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\u201358 (2010)","key":"14_CR8"},{"key":"14_CR9","volume-title":"Parts: A Study in Ontology","author":"P. Simons","year":"1987","unstructured":"Simons, P.: Parts: A Study in Ontology. Clarendon Press, Oxford (1987)"},{"issue":"3","key":"14_CR10","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/S0169-023X(96)00017-1","volume":"20","author":"A.C. Varzi","year":"1996","unstructured":"Varzi, A.C.: Parts, wholes, and part-whole relations: The prospects of mereotopology. Data and Knowledge Engineering\u00a020(3), 259\u2013286 (1996)","journal-title":"Data and Knowledge Engineering"},{"doi-asserted-by":"crossref","unstructured":"Johansson, I.: On the transitivity of the parthood relations. In: Hochberg, H., Mulligan, K. (eds.) Relations and Predicates, pp. 161\u2013181. Ontos Verlag (2004)","key":"14_CR11","DOI":"10.1515\/9783110326857.161"},{"key":"14_CR12","first-page":"79","volume-title":"Parts of Classes","author":"D. Lewis","year":"1991","unstructured":"Lewis, D.: Parts of Classes, pp. 79\u201393. Blackwell Publishers, Oxford (1991)"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/S0950-5849(00)00175-0","volume":"43","author":"A.L. Opdahl","year":"2001","unstructured":"Opdahl, A.L., Henderson-Sellers, B., Barbier, F.: Ontological analysis of whole-part relationships in OO-models. Information and Software Technology\u00a043, 387\u2013399 (2001)","journal-title":"Information and Software Technology"},{"unstructured":"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\u201310 (2004)","key":"14_CR14"},{"issue":"1","key":"14_CR15","first-page":"31","volume":"3","author":"S. Schulz","year":"2009","unstructured":"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\u00a03(1), 31\u201345 (2009)","journal-title":"Elec. J. of Com., Inf. and Innovation in Health"},{"unstructured":"Guizzardi, G.: On the Representation of Quantities and their Parts in Conceptual Modeling. In: Procs. of the Sixth Int. Conference (FOIS 2010), pp. 103\u2013116. IOS Press (2010)","key":"14_CR16"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1006\/ijhc.1995.1079","volume":"43","author":"P. Gerstl","year":"1995","unstructured":"Gerstl, P., Pribbenow, S.: Midwinters, End Games, and Body Parts: a Classification of Part-whole Relations. Int. Journal of Human-Computer Studies\u00a043, 865\u2013889 (1995)","journal-title":"Int. Journal of Human-Computer Studies"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31175-8_1","volume-title":"Controlled Natural Language","author":"K. Angelov","year":"2012","unstructured":"Angelov, K., Enache, R.: Typeful Ontologies with Direct Multilingual Verbalization. In: Rosner, M., Fuchs, N.E. (eds.) CNL 2010. LNCS, vol.\u00a07175, pp. 1\u201320. Springer, Heidelberg (2012)"},{"unstructured":"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)","key":"14_CR19"},{"issue":"1","key":"14_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1017\/S0956796803004921","volume":"14","author":"A.W. Appel","year":"2004","unstructured":"Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. Journal of Functional Programming\u00a014(1), 3\u201319 (2004)","journal-title":"Journal of Functional Programming"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-69149-5_19","volume-title":"Verified Software: Theories, Tools, Experiments","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Th\u00e9ry, L.: Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 173\u2013181. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. An EATCS series. Springer (2004)","key":"14_CR22","DOI":"10.1007\/978-3-662-07964-5"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-35786-2_11","volume-title":"Conceptual Structures for STEM Research and Education","author":"R. Dapoigny","year":"2013","unstructured":"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.\u00a07735, pp. 135\u2013152. Springer, Heidelberg (2013)"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"issue":"4","key":"14_CR25","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B. Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science\u00a021(4), 795\u2013825 (2011)","journal-title":"Mathematical Structures in Computer Science"},{"unstructured":"Sowa, J.F.: Using a lexicon of canonical graphs in a semantic interpreter. In: Relational Models of the Lexicon, pp. 113\u2013137. Cambridge University Press (1988)","key":"14_CR26"},{"unstructured":"Masolo, C., Borgo, S., Gangemi, A., Guarino, N., Oltramari, A.: Ontology Library (D18), Laboratory for Applied Ontology-ISTC-CNR (2003)","key":"14_CR27"},{"key":"14_CR28","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45810-7_18","volume-title":"Knowledge Engineering and Knowledge Management. Ontologies and the Semantic Web","author":"A. Gangemi","year":"2002","unstructured":"Gangemi, A., Guarino, N., Masolo, C., Oltramari, A., Schneider, L.: Sweetening ontologies with DOLCE. In: G\u00f3mez-P\u00e9rez, A., Benjamins, V.R. (eds.) EKAW 2002. LNCS (LNAI), vol.\u00a02473, pp. 166\u2013181. Springer, Heidelberg (2002)"},{"key":"14_CR29","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/S0169-023X(96)00015-8","volume":"20","author":"B. Smith","year":"1996","unstructured":"Smith, B.: Mereotopology: A Theory of Parts and Boundaries. Data and Knowledge Engineering\u00a020, 287\u2013303 (1996)","journal-title":"Data and Knowledge Engineering"},{"unstructured":"Varzi, A.C.: Mereology. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2012), \n                      http:\/\/plato.stanford.edu\/archives\/win2012\/entries\/mereology","key":"14_CR30"},{"issue":"6-7","key":"14_CR31","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1002\/cfg.429","volume":"5","author":"A. Kumar","year":"2004","unstructured":"Kumar, A., Smith, B., Novotny, D.: Biomedical Informatics and granularity. Comparative and Functional Genomics\u00a05(6-7), 501\u2013508 (2004)","journal-title":"Comparative and Functional Genomics"},{"issue":"3","key":"14_CR32","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/j.jbi.2005.08.010","volume":"39","author":"A. Rector","year":"2006","unstructured":"Rector, A., Rogers, J., Bittner, T.: Granularity, scale and collectivity: When size does and does not matter. J. of Biomedical Informatics\u00a039(3), 333\u2013349 (2006)","journal-title":"J. of Biomedical Informatics"},{"issue":"1","key":"14_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artmed.2005.07.004","volume":"36","author":"M. Donnelly","year":"2005","unstructured":"Donnelly, M., Bittner, T., Rosse, C.: A formal theory for spatial representation and reasoning in biomedical ontologies. Artificial Intelligence in Medicine\u00a036(1), 1\u201327 (2005)","journal-title":"Artificial Intelligence in Medicine"},{"issue":"1","key":"14_CR34","first-page":"41","volume":"2","author":"M. Sozeau","year":"2009","unstructured":"Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning\u00a02(1), 41\u201362 (2009)","journal-title":"Journal of Formalized Reasoning"}],"container-title":["Lecture Notes in Computer Science","Graph-Based Representation and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08389-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T19:40:32Z","timestamp":1674157232000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-08389-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319083889","9783319083896"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08389-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}