Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

2015 | OriginalPaper | Chapter

A Coq-Based Axiomatization of Tarski’s Mereogeometry

Authors: Richard Dapoigny, Patrick Barlatier

Published in: Spatial Information Theory

Publisher: Springer International Publishing

share
SHARE

Abstract

During the last decade, the domain of Qualitative Spatial Reasoning, has known a renewal of interest for mereogeometry, a theory that has been initiated by Tarski. Mereogeometry relies on mereology, the Leśniewski’s theory of parts and wholes that is further extended with geometrical primitives and appropriate definitions. However, most approaches (i) depart from the original Leśniewski’s mereology which does not assume usual sets as a basis, (ii) restrict the logical power of mereology to a mere theory of part-whole relations and (iii) require the introduction of a connection relation. Moreover, the seminal paper of Tarki shows up unclear foundations and we argue that mereogeometry as it is introduced by Tarski, can be more suited to extend the whole theory of Leśniewski. For that purpose, we investigate a type-theoretical representation of space more closely related with the original ideas of Leśniewski and expressed with the Coq language. We show that (i) it can be given a more clear foundation, (ii) it can be based on three axioms instead of four and (iii) it can serve as a basis for spatial reasoning with full compliance with Leśniewski’s systems.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Testen Sie jetzt 15 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




Testen Sie jetzt 15 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Testen Sie jetzt 15 Tage kostenlos.

Footnotes
1
Most descriptions suffer from the misunderstanding that mereology is formally nothing more than a particular elementary theory of partial ordering.
 
2
The two argument categories are on the right side and the resulting category on the left side.
 
3
This is partly due to the destruction of most of his work during the second world war and to the difficulty to assess protothetic.
 
4
Known as Girard–Reynolds polymorphic lambda calculus. It extends STT by the introduction of a mechanism of universal quantification over types (second-order) and is itself extended in CIC.
 
5
Also called sort.
 
6
Called spheres in Tarski’s paper.
 
Literature
1.
go back to reference Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14(1), 3–19 (2004). Cambridge University Press CrossRefMathSciNetMATH Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14(1), 3–19 (2004). Cambridge University Press CrossRefMathSciNetMATH
2.
go back to reference 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) 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)
3.
go back to reference 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–126. Universidad Pais Vasco, San Sebastian (1995) 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–126. Universidad Pais Vasco, San Sebastian (1995)
5.
go back to reference Bennett, B.: A categorical axiomatisation of region-based geometry. Fundam. Informaticae 46(1–2), 145–158 (2001) MATH Bennett, B.: A categorical axiomatisation of region-based geometry. Fundam. Informaticae 46(1–2), 145–158 (2001) MATH
6.
go back to reference Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004) CrossRef Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004) CrossRef
7.
go back to reference 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) CrossRef 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) CrossRef
9.
go back to reference Betti, A.: Leśniewski, 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ński, pp. 242–258. Palgrave Macmillan, Basingstoke (2013) Betti, A.: Leśniewski, 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ński, pp. 242–258. Palgrave Macmillan, Basingstoke (2013)
10.
go back to reference 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–229. Morgan Kaufmann (1996) 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–229. Morgan Kaufmann (1996)
13.
go back to reference Clay, R.E.: The consistency of Leśniewski’s mereology relative to the real number system. J. Symbolic Logic 33, 251–257 (1968) CrossRefMathSciNetMATH Clay, R.E.: The consistency of Leśniewski’s mereology relative to the real number system. J. Symbolic Logic 33, 251–257 (1968) CrossRefMathSciNetMATH
14.
16.
go back to reference Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG-88. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990) CrossRef Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG-88. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990) CrossRef
18.
go back to reference Eschenbach, C., Heydrich, W.: Classical mereology and restricted domains. Int. J. Hum. Comput. Stud. 43(56), 723–740 (1995) CrossRef Eschenbach, C., Heydrich, W.: Classical mereology and restricted domains. Int. J. Hum. Comput. Stud. 43(56), 723–740 (1995) CrossRef
19.
go back to reference Gerla, G.: Pointless geometries. In: Buekenhout, F. (ed.) Handbook of Incidence Geometry, pp. 1015–1031. Elsevier, North-Holland (1995) CrossRef Gerla, G.: Pointless geometries. In: Buekenhout, F. (ed.) Handbook of Incidence Geometry, pp. 1015–1031. Elsevier, North-Holland (1995) CrossRef
20.
go back to reference Gessler, N.: Introduction à l’oeuvre de S. Leśniewski. Part III: La méréologie. CdRS, Université de Neuchâtel (2005) Gessler, N.: Introduction à l’oeuvre de S. Leśniewski. Part III: La méréologie. CdRS, Université de Neuchâtel (2005)
21.
go back to reference Gruszczy \(\grave{{\rm n}}\)ski, R., Pietruszczak, R.: Full development of tarski’s geometry of solids. Bull. Symbolic Logic 14(4), 481–540 (2008) Gruszczy \(\grave{{\rm n}}\)ski, R., Pietruszczak, R.: Full development of tarski’s geometry of solids. Bull. Symbolic Logic 14(4), 481–540 (2008)
22.
go back to reference Hahmann, T., Grüninger, 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–62. IGI Publishing, USA (2012) CrossRef Hahmann, T., Grüninger, 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–62. IGI Publishing, USA (2012) CrossRef
23.
24.
go back to reference Hofmann, M.: Extensional concepts in intensional type theory. Ph.d. thesis, University of Edinburgh (1995) Hofmann, M.: Extensional concepts in intensional type theory. Ph.d. thesis, University of Edinburgh (1995)
25.
go back to reference Kortenkamp, D., Bonasso, R.P., Murphy, R. (eds.): Artificial Intelligence and Mobile Robots: Case Studies of Successful Robot Systems. MIT Press, Cambridge (1998) Kortenkamp, D., Bonasso, R.P., Murphy, R. (eds.): Artificial Intelligence and Mobile Robots: Case Studies of Successful Robot Systems. MIT Press, Cambridge (1998)
26.
go back to reference 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–404. Morgan Kaufmann, San Mateo (1987) 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–404. Morgan Kaufmann, San Mateo (1987)
28.
go back to reference Leśniewski, S.: Podstawy ogólnej 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śniewski, Collected Works, vol. 1, pp. 129–173. Kluwer, Dordrecht (1992)) Leśniewski, S.: Podstawy ogólnej 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śniewski, Collected Works, vol. 1, pp. 129–173. Kluwer, Dordrecht (1992))
29.
go back to reference Leśniewski, S.: Einleitende Bemerkungen zur Fortsezung meiner Miteilung u.d.T. “Grundzüge eines neuen Systems der Grundlagen der Mathematik”. Collectanea Logica I, 1–60 (1938) Leśniewski, S.: Einleitende Bemerkungen zur Fortsezung meiner Miteilung u.d.T. “Grundzüge eines neuen Systems der Grundlagen der Mathematik”. Collectanea Logica I, 1–60 (1938)
30.
go back to reference Oury, N.: Extensionality in the calculus of constructions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 278–293. Springer, Heidelberg (2005) CrossRef Oury, N.: Extensionality in the calculus of constructions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 278–293. Springer, Heidelberg (2005) CrossRef
31.
go back to reference Quine, W.: Unification of universes in set theory. J. Symb. Logic 21, 216 (1956) CrossRef Quine, W.: Unification of universes in set theory. J. Symb. Logic 21, 216 (1956) CrossRef
32.
go back to reference 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–176. Morgan Kaufmann, San Mateo (1992) 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–176. Morgan Kaufmann, San Mateo (1992)
35.
go back to reference Simons, P.: Parts: A Study in Ontology. Clarendon Press, Oxford (1987) Simons, P.: Parts: A Study in Ontology. Clarendon Press, Oxford (1987)
36.
go back to reference Simons, P.M.: Nominalism in Poland. In: Srzednicki, J.T.J., Stachniak, Z. (eds.) Leśniewski’s Systems Protothetic. Nijhoff International Philosophy Series, vol. 54, pp. 1–22. Springer, Netherlands (1998) CrossRef Simons, P.M.: Nominalism in Poland. In: Srzednicki, J.T.J., Stachniak, Z. (eds.) Leśniewski’s Systems Protothetic. Nijhoff International Philosophy Series, vol. 54, pp. 1–22. Springer, Netherlands (1998) CrossRef
39.
go back to reference Sobociński, B.: On the single axioms of protothetic I. Notre-Dame J. Formal Logic 1, 52–73 (1960) CrossRef Sobociński, B.: On the single axioms of protothetic I. Notre-Dame J. Formal Logic 1, 52–73 (1960) CrossRef
40.
go back to reference Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reasoning 2(1), 41–62 (2009) MathSciNetMATH Sozeau, M.: A new look at generalized rewriting in type theory. J. Formalized Reasoning 2(1), 41–62 (2009) MathSciNetMATH
41.
go back to reference Tarski, A.: Sur le terme primitif de la Logistique. Fundam. Math. 4, 196–200 (1923) Tarski, A.: Sur le terme primitif de la Logistique. Fundam. Math. 4, 196–200 (1923)
42.
go back to reference Tarski, A.: Les fondements de la géométrie des corps (Foundations of the geometry of solids). In: Ksiega Pamiatkowa Pierwszego Polskiego Zjazdu Matematycznego, vol. 7, pp. 29–33 (1929) Tarski, A.: Les fondements de la géométrie des corps (Foundations of the geometry of solids). In: Ksiega Pamiatkowa Pierwszego Polskiego Zjazdu Matematycznego, vol. 7, pp. 29–33 (1929)
43.
go back to reference Tarski, A.: Foundations of the geometry of solids. In: Tarski, A. (ed.) Logics, Semantics Metamathematics. Papers from 1923–1938 by Alfred Tarski. Clarendon Press, Oxford (1956) Tarski, A.: Foundations of the geometry of solids. In: Tarski, A. (ed.) Logics, Semantics Metamathematics. Papers from 1923–1938 by Alfred Tarski. Clarendon Press, Oxford (1956)
44.
go back to reference Tarski, A.: On the foundation of Boolean algebra. In: Woodger, J.H. (ed.) Logic, Semantics, Metamathematics: Papers from 1923 to 1938, pp. 320–341. Clarendon Press, Oxford (1956) Tarski, A.: On the foundation of Boolean algebra. In: Woodger, J.H. (ed.) Logic, Semantics, Metamathematics: Papers from 1923 to 1938, pp. 320–341. Clarendon Press, Oxford (1956)
45.
go back to reference Varzi, A.C.: Parts, wholes, and part-whole relations: the prospects of mereotopology. Data Knowl. Eng. 20(3), 259–286 (1996) CrossRefMATH Varzi, A.C.: Parts, wholes, and part-whole relations: the prospects of mereotopology. Data Knowl. Eng. 20(3), 259–286 (1996) CrossRefMATH
Metadata
Title
A Coq-Based Axiomatization of Tarski’s Mereogeometry
Authors
Richard Dapoigny
Patrick Barlatier
Copyright Year
2015
DOI
https://doi.org/10.1007/978-3-319-23374-1_6

Premium Partner