{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:17:13Z","timestamp":1742995033676,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319233734"},{"type":"electronic","value":"9783319233741"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23374-1_6","type":"book-chapter","created":{"date-parts":[[2015,9,29]],"date-time":"2015-09-29T13:15:10Z","timestamp":1443532510000},"page":"108-129","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Coq-Based Axiomatization of Tarski\u2019s Mereogeometry"],"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","published-online":{"date-parts":[[2015,12,15]]},"reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1017\/S0956796803004921","volume":"14","author":"AW Appel","year":"2004","unstructured":"Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14(1), 3\u201319 (2004). Cambridge University Press","journal-title":"J. Funct. Program."},{"key":"6_CR2","unstructured":"Asher, N., Vieu, L.: Toward a geometry of common sense: a semantics and a complete axiomatization of mereotopology. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI-95), Montreal (1995)"},{"key":"6_CR3","series-title":"ILCLI Series I","first-page":"69","volume-title":"Semantics and Pragmatics of Natural Language: Logical and Computational Aspects","author":"M Aurnague","year":"1995","unstructured":"Aurnague, M., Vieu, L.: A theory of space-time for natural language semantics. In: Korta, K., Larrazabal, J.M. (eds.) Semantics and Pragmatics of Natural Language: Logical and Computational Aspects. ILCLI Series I, pp. 69\u2013126. Universidad Pais Vasco, San Sebastian (1995)"},{"issue":"2","key":"6_CR4","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"issue":"1\u20132","key":"6_CR5","first-page":"145","volume":"46","author":"B Bennett","year":"2001","unstructured":"Bennett, B.: A categorical axiomatisation of region-based geometry. Fundam. Informaticae 46(1\u20132), 145\u2013158 (2001)","journal-title":"Fundam. Informaticae"},{"key":"6_CR6","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"6_CR7","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. 4171, pp. 173\u2013181. Springer, Heidelberg (2008)"},{"issue":"2","key":"6_CR8","doi-asserted-by":"publisher","first-page":"230","DOI":"10.2178\/bsl\/1333560806","volume":"18","author":"A Betti","year":"2012","unstructured":"Betti, A., Loeb, I.: On Tarski\u2019s foundations of the geometry of solids. Bull. Symbolic Logic 18(2), 230\u2013260 (2012)","journal-title":"Bull. Symbolic Logic"},{"key":"6_CR9","first-page":"242","volume-title":"The History and Philosophy of Polish Logic: Essays in Honour of Jan Wole\u0144ski","author":"A Betti","year":"2013","unstructured":"Betti, A.: Le\u015bniewski, Tarski and the axioms of mereology. Chap. 11. In: Mulligan, K., et al. (eds.) The History and Philosophy of Polish Logic: Essays in Honour of Jan Wole\u0144ski, pp. 242\u2013258. Palgrave Macmillan, Basingstoke (2013)"},{"key":"6_CR10","unstructured":"Borgo, S., Guarino, N., Masolo, C.: A pointless theory of space based on strong congruence and connection. In: Proceedings of 5th International Conference on Principle of Knowledge Representation and Reasoning (KR 1996), pp. 220\u2013229. Morgan Kaufmann (1996)"},{"issue":"4","key":"6_CR11","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1017\/S1755020310000110","volume":"3","author":"S Borgo","year":"2010","unstructured":"Borgo, S., Masolo, C.: Full mereogeometries. Rev. Symbolic Logic 3(4), 521\u2013567 (2010)","journal-title":"Rev. Symbolic Logic"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56\u201368 (1940)","journal-title":"J. Symbolic Logic"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"251","DOI":"10.2307\/2269870","volume":"33","author":"RE Clay","year":"1968","unstructured":"Clay, R.E.: The consistency of Le\u015bniewski\u2019s mereology relative to the real number system. J. Symbolic Logic 33, 251\u2013257 (1968)","journal-title":"J. Symbolic Logic"},{"issue":"4","key":"6_CR14","doi-asserted-by":"publisher","first-page":"638","DOI":"10.2307\/2272847","volume":"39","author":"RE Clay","year":"1974","unstructured":"Clay, R.E.: Relation of Le\u015bniewski\u2019s mereology to boolean algebra. J. Symbolic Logic 39(4), 638\u2013648 (1974)","journal-title":"J. Symbolic Logic"},{"issue":"2\u20133","key":"6_CR15","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2\u20133), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG-88. LNCS, vol. 417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"6_CR17","unstructured":"Dapoigny, R., Barlatier, P.: Tarski$$\\_$$Mereogeometry, University of Savoie (2015). http:\/\/www.polytech.univ-savoie.fr\/index.php?id=listic-logiciels-lib-spatial&L=1"},{"issue":"56","key":"6_CR18","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1006\/ijhc.1995.1071","volume":"43","author":"C Eschenbach","year":"1995","unstructured":"Eschenbach, C., Heydrich, W.: Classical mereology and restricted domains. Int. J. Hum. Comput. Stud. 43(56), 723\u2013740 (1995)","journal-title":"Int. J. Hum. Comput. Stud."},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"1015","DOI":"10.1016\/B978-044488355-1\/50020-7","volume-title":"Handbook of Incidence Geometry","author":"G Gerla","year":"1995","unstructured":"Gerla, G.: Pointless geometries. In: Buekenhout, F. (ed.) Handbook of Incidence Geometry, pp. 1015\u20131031. Elsevier, North-Holland (1995)"},{"key":"6_CR20","unstructured":"Gessler, N.: Introduction \u00e0 l\u2019oeuvre de S. Le\u015bniewski. Part III: La m\u00e9r\u00e9ologie. CdRS, Universit\u00e9 de Neuch\u00e2tel (2005)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Gruszczy$$\\grave{{\\rm n}}$$ski, R., Pietruszczak, R.: Full development of tarski\u2019s geometry of solids. Bull. Symbolic Logic 14(4), 481\u2013540 (2008)","DOI":"10.2178\/bsl\/1231081462"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4018\/978-1-61692-868-1.ch001","volume-title":"Qualitative Spatio-Temporal Representation and Reasoning: Trends and Future Directions","author":"T Hahmann","year":"2012","unstructured":"Hahmann, T., Gr\u00fcninger, M.: Region-based theories of space: mereotopology and beyond. In: Hazarika, S.M. (ed.) Qualitative Spatio-Temporal Representation and Reasoning: Trends and Future Directions, pp. 1\u201362. IGI Publishing, USA (2012)"},{"key":"6_CR23","doi-asserted-by":"crossref","first-page":"323","DOI":"10.4064\/fm-52-3-323-344","volume":"52","author":"L Henkin","year":"1963","unstructured":"Henkin, L.: A theory of propositional types. Fundam. Math. 52, 323\u2013334 (1963). Errata 53, 119","journal-title":"Fundam. Math."},{"key":"6_CR24","unstructured":"Hofmann, M.: Extensional concepts in intensional type theory. Ph.d. thesis, University of Edinburgh (1995)"},{"volume-title":"Artificial Intelligence and Mobile Robots: Case Studies of Successful Robot Systems","year":"1998","key":"6_CR25","unstructured":"Kortenkamp, D., Bonasso, R.P., Murphy, R. (eds.): Artificial Intelligence and Mobile Robots: Case Studies of Successful Robot Systems. MIT Press, Cambridge (1998)"},{"key":"6_CR26","unstructured":"Kuipers, B.J., Byun, Y.T.: A qualitative approach to robot exploration and map learning. In: Proceedings of the IEEE Workshop on Spatial Reasoning and Multi-Sensor Fusion, pp. 390\u2013404. Morgan Kaufmann, San Mateo (1987)"},{"issue":"3","key":"6_CR27","doi-asserted-by":"publisher","first-page":"321","DOI":"10.2307\/2270898","volume":"34","author":"C Lejewski","year":"1969","unstructured":"Lejewski, C.: Consistency of Le\u015bniewski\u2019s mereology. J. Symbolic Logic 34(3), 321\u2013328 (1969)","journal-title":"J. Symbolic Logic"},{"key":"6_CR28","unstructured":"Le\u015bniewski, S.: Podstawy og\u00f3lnej teoryi mnogosci. I, Moskow: Prace Polskiego Kola Naukowego w Moskwie, Sekcya matematyczno-przyrodnicza (1916). (English translation by Barnett, D.I.: Foundations of the general theory of sets. I. In: Surma, S.J., Srzednicki, J., Barnett, D.I., Rickey, F.V. (eds.) S. Le\u015bniewski, Collected Works, vol. 1, pp. 129\u2013173. Kluwer, Dordrecht (1992))"},{"key":"6_CR29","first-page":"1","volume":"I","author":"S Le\u015bniewski","year":"1938","unstructured":"Le\u015bniewski, S.: Einleitende Bemerkungen zur Fortsezung meiner Miteilung u.d.T. \u201cGrundz\u00fcge eines neuen Systems der Grundlagen der Mathematik\u201d. Collectanea Logica I, 1\u201360 (1938)","journal-title":"Collectanea Logica"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11541868_18","volume-title":"Theorem Proving in Higher Order Logics","author":"N Oury","year":"2005","unstructured":"Oury, N.: Extensionality in the calculus of constructions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 278\u2013293. Springer, Heidelberg (2005)"},{"key":"6_CR31","doi-asserted-by":"publisher","first-page":"216","DOI":"10.2307\/2268792","volume":"21","author":"W Quine","year":"1956","unstructured":"Quine, W.: Unification of universes in set theory. J. Symb. Logic 21, 216 (1956)","journal-title":"J. Symb. Logic"},{"key":"6_CR32","unstructured":"Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Proceedings of 3rd International Conference on Knowledge Representation and Reasoning, pp. 165\u2013176. Morgan Kaufmann, San Mateo (1992)"},{"key":"6_CR33","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF02120674","volume":"36","author":"VF Rickey","year":"1977","unstructured":"Rickey, V.F.: A survey of Le\u015bniewski\u2019s logic. Stud. Logica 36, 407\u2013426 (1977)","journal-title":"Stud. Logica"},{"issue":"3","key":"6_CR34","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1093\/logcom\/11.3.483","volume":"11","author":"JP Seldin","year":"2001","unstructured":"Seldin, J.P.: Extensional set equality in the calculus of constructions. J. Log. Comput. 11(3), 483\u2013493 (2001)","journal-title":"J. Log. Comput."},{"key":"6_CR35","volume-title":"Parts: A Study in Ontology","author":"P Simons","year":"1987","unstructured":"Simons, P.: Parts: A Study in Ontology. Clarendon Press, Oxford (1987)"},{"key":"6_CR36","series-title":"Nijhoff International Philosophy Series","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-94-011-5736-0_1","volume-title":"Le\u015bniewski\u2019s Systems Protothetic","author":"PM Simons","year":"1998","unstructured":"Simons, P.M.: Nominalism in Poland. In: Srzednicki, J.T.J., Stachniak, Z. (eds.) Le\u015bniewski\u2019s Systems Protothetic. Nijhoff International Philosophy Series, vol. 54, pp. 1\u201322. Springer, Netherlands (1998)"},{"issue":"1","key":"6_CR37","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF00139700","volume":"2","author":"VF Sinisi","year":"1983","unstructured":"Sinisi, V.F.: Le\u015bniewski\u2019s foundations of mathematics. Topoi 2(1), 3\u201352 (1983)","journal-title":"Topoi"},{"key":"6_CR38","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/BF02272275","volume":"1","author":"J Slupecki","year":"1953","unstructured":"Slupecki, J.: S. Le\u015bniewski\u2019s protothetics. Stud. Logica 1, 44\u2013112 (1953)","journal-title":"Stud. Logica"},{"key":"6_CR39","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1305\/ndjfl\/1093956428","volume":"1","author":"B Soboci\u0144ski","year":"1960","unstructured":"Soboci\u0144ski, B.: On the single axioms of protothetic I. Notre-Dame J. Formal Logic 1, 52\u201373 (1960)","journal-title":"Notre-Dame J. Formal Logic"},{"issue":"1","key":"6_CR40","first-page":"41","volume":"2","author":"M Sozeau","year":"2009","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reasoning 2(1), 41\u201362 (2009)","journal-title":"J. Formalized Reasoning"},{"key":"6_CR41","doi-asserted-by":"crossref","first-page":"196","DOI":"10.4064\/fm-4-1-196-200","volume":"4","author":"A Tarski","year":"1923","unstructured":"Tarski, A.: Sur le terme primitif de la Logistique. Fundam. Math. 4, 196\u2013200 (1923)","journal-title":"Fundam. Math."},{"key":"6_CR42","unstructured":"Tarski, A.: Les fondements de la g\u00e9om\u00e9trie des corps (Foundations of the geometry of solids). In: Ksiega Pamiatkowa Pierwszego Polskiego Zjazdu Matematycznego, vol. 7, pp. 29\u201333 (1929)"},{"key":"6_CR43","volume-title":"Logics, Semantics Metamathematics. Papers from 1923\u20131938 by Alfred Tarski","author":"A Tarski","year":"1956","unstructured":"Tarski, A.: Foundations of the geometry of solids. In: Tarski, A. (ed.) Logics, Semantics Metamathematics. Papers from 1923\u20131938 by Alfred Tarski. Clarendon Press, Oxford (1956)"},{"key":"6_CR44","first-page":"320","volume-title":"Logic, Semantics, Metamathematics: Papers from 1923 to 1938","author":"A Tarski","year":"1956","unstructured":"Tarski, A.: On the foundation of Boolean algebra. In: Woodger, J.H. (ed.) Logic, Semantics, Metamathematics: Papers from 1923 to 1938, pp. 320\u2013341. Clarendon Press, Oxford (1956)"},{"issue":"3","key":"6_CR45","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/S0169-023X(96)00017-1","volume":"20","author":"AC Varzi","year":"1996","unstructured":"Varzi, A.C.: Parts, wholes, and part-whole relations: the prospects of mereotopology. Data Knowl. Eng. 20(3), 259\u2013286 (1996)","journal-title":"Data Knowl. Eng."}],"container-title":["Lecture Notes in Computer Science","Spatial Information Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23374-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T15:43:26Z","timestamp":1676475806000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23374-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319233734","9783319233741"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23374-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"15 December 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}