Description

• Title:
  A Monadic Second-Order Version of Tarski’s Geometry of Solids
• Creator:
  Barlatier, Patrick;
  Dapoigny
• Description:
  In this paper, we are concerned with the development of a general set theory using the single axiom version of Leśniewski’s mereology. The specification of mereology, and further of Tarski’s geometry of solids will rely on the Calculus of Inductive Constructions (CIC). In the first part, we provide a specification of Leśniewski’s mereology as a model for an atomless Boolean algebra using Clay’s ideas. In the second part, we interpret Leśniewski’s mereology in monadic second-order logic using names and develop a full version of mereology referred to as CIC-based Monadic Mereology (λ-MM) allowing an expressive theory while involving only two axioms. In the third part, we propose a modeling of Tarski’s solid geometry relying on λ-MM. It is intended to serve as a basis for spatial reasoning. All parts have been proved using a translation in type theory.
• Object availability:
  free access
• Rights:
  Prawa autorskie (c) 2023 Patrick Barlatier, Richard Dapoigny;
  https://creativecommons.org/licenses/by-nd/4.0
• Date:
  2023.10.19
• Type:
  info:eu-repo/semantics/article;
  info:eu-repo/semantics/publishedVersion
• Language:
  English
• Source:
  Logic and Logical Philosophy; Vol. 33 No. 1 (2024): March; 55-99;
  Logic and Logical Philosophy; Tom 33 Nr 1 (2024): Marzec; 55-99;
  2300-9802;
  1425-3305
• Format:
  application/pdf
• Publisher:
  Uniwersytet Mikołaja Kopernika w Toruniu
• Relation: https://apcz.umk.pl/LLP/article/view/35945/36789
• Subject:
  mereology;
  monadic second-order logic;
  geometry of solids;
  calculus of inductive constructions;
  theorem prover;
  type theory
• Identifier: https://apcz.umk.pl/LLP/article/view/35945
• Data provider:
  Akademicka Platforma Czasopism
• Can I use it?:
  seek permission
• Type:
  text