Check in the files I thought I checked in 65c1e0b

src/common logic/continuant-mereology.cl

@@ -1,14 +1,14 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2021/11/12
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text
 
   (cl:ttl https://basic-formal-ontology.org/2020/formulas/clif/continuant-mereology.cl
 
-   (cl:outdiscourse temporal-part-of exists-at has-proper-continuant-part proper-continuant-part-of instance-of has-continuant-part continuant-part-of)
+   (cl:outdiscourse occupies-spatial-region temporal-part-of exists-at has-proper-continuant-part proper-continuant-part-of instance-of has-continuant-part continuant-part-of)
 
   (cl:comment "continuant-part-of and has-continuant-part are inverse relations [eld-1]"
     (forall (t a b)
@@ -163,6 +163,30 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
       (proper-continuant-part-of a c t))))
 
 
+  (cl:comment "A fiat line occupies a one-dimensional spatial region [kcq-1]"
+    (forall (x t)
+     (if (instance-of x fiat-line t)
+      (exists (s tp)
+       (and (temporal-part-of tp t) (occupies-spatial-region x s tp)
+        (instance-of s one-dimensional-spatial-region tp))))))
+
+
+  (cl:comment "A fiat point occupies a zero-dimensional spatial region [alm-1]"
+    (forall (x t)
+     (if (instance-of x fiat-point t)
+      (exists (tp s)
+       (and (temporal-part-of tp t) (occupies-spatial-region x s tp)
+        (instance-of s zero-dimensional-spatial-region tp))))))
+
+
+  (cl:comment "A fiat surface occupies a two-dimensional spatial region [fpl-1]"
+    (forall (x t)
+     (if (instance-of x fiat-surface t)
+      (exists (s tp)
+       (and (temporal-part-of tp t) (occupies-spatial-region x s tp)
+        (instance-of s two-dimensional-spatial-region tp))))))
+
+
   (cl:comment "If a has-continuant-part b then if a is an instance of material-entity then b is an instance of site or continuant-fiat-boundary or material-entity  [mic-1]"
     (forall (p q t)
      (if
@@ -193,6 +217,50 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
       (= a b))))
 
 
+  (cl:comment "The dimensionality of the region of something occupying a one dimensional spatial region does not change [qfe-1]"
+    (forall (m s)
+     (if
+      (exists (t)
+       (and (occupies-spatial-region m s t)
+        (instance-of s one-dimensional-spatial-region t)))
+      (forall (t1 s1)
+       (if (occupies-spatial-region m s1 t1)
+        (instance-of s1 one-dimensional-spatial-region t1))))))
+
+
+  (cl:comment "The dimensionality of the region of something occupying a two dimensional spatial region does not change [dor-1]"
+    (forall (m s)
+     (if
+      (exists (t)
+       (and (occupies-spatial-region m s t)
+        (instance-of s two-dimensional-spatial-region t)))
+      (forall (t1 s1)
+       (if (occupies-spatial-region m s1 t1)
+        (instance-of s1 two-dimensional-spatial-region t1))))))
+
+
+  (cl:comment "The dimensionality of the region of something occupying a zero dimensional spatial region does not change [fok-1]"
+    (forall (m s)
+     (if
+      (exists (t)
+       (and (occupies-spatial-region m s t)
+        (instance-of s zero-dimensional-spatial-region t)))
+      (forall (t1 s1)
+       (if (occupies-spatial-region m s1 t1)
+        (instance-of s1 zero-dimensional-spatial-region t1))))))
+
+
+  (cl:comment "The dimensionality of the region of something occupying a three dimensional spatial region does not change [rlf-1]"
+    (forall (m s)
+     (if
+      (exists (t)
+       (and (occupies-spatial-region m s t)
+        (instance-of s three-dimensional-spatial-region t)))
+      (forall (t1 s1)
+       (if (occupies-spatial-region m s1 t1)
+        (instance-of s1 three-dimensional-spatial-region t1))))))
+
+
   (cl:comment "If a material entity has a proper part, then at least one of its proper parts is not an immaterial entity [adm-1]"
     (forall (m t)
      (if

src/common logic/existence-instantiation.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2021/11/12
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text

src/common logic/generic-dependence.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2021/11/12
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text

src/common logic/history.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2022/09/23
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text

src/common logic/material-entity.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2022/11/01
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text

src/common logic/occurrent-mereology.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2022/11/01
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text
@@ -48,6 +48,13 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
       (forall (t) (if (exists-at o1 t) (exists-at o2 t))))))
 
 
+  (cl:comment "If a occurrent-part-of b then if a is an instance of temporal-region then b is an instance of temporal-region, and vice-versa [gjl-2]"
+    (forall (p q)
+     (if (occurrent-part-of p q)
+      (iff (instance-of p temporal-region p)
+       (instance-of q temporal-region q)))))
+
+
   (cl:comment "occurrent-part-of has domain occurrent and range occurrent [zmr-1]"
     (forall (a b)
      (if (occurrent-part-of a b)
@@ -84,11 +91,12 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
         (occurrent-part-of pb p))))))
 
 
-  (cl:comment "If a occurrent-part-of b then if a is an instance of temporal-region then b is an instance of temporal-region, and vice-versa [gjl-1]"
-    (forall (p q)
-     (if (occurrent-part-of p q)
-      (iff (exists (t) (instance-of p temporal-region t))
-       (exists (t) (instance-of q temporal-region t))))))
+  (cl:comment "definition of temporal part for temporal regions [cmy-2]"
+    (forall (b c)
+     (if
+      (and (instance-of b temporal-region b)
+       (instance-of c temporal-region c))
+      (iff (temporal-part-of b c) (occurrent-part-of b c)))))
 
 
   (cl:comment "If a has-occurrent-part b then if a is an instance of process-boundary then b is an instance of process-boundary [hdk-1]"
@@ -105,14 +113,6 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
        (exists (t) (instance-of q spatiotemporal-region t))))))
 
 
-  (cl:comment "definition of temporal part for temporal regions [cmy-1]"
-    (forall (b c)
-     (if
-      (and (exists (t) (instance-of b temporal-region t))
-       (exists (t) (instance-of c temporal-region t)))
-      (iff (temporal-part-of b c) (occurrent-part-of b c)))))
-
-
   (cl:comment "If a has-occurrent-part b then if a is an instance of process then b is an instance of process or process-boundary  [ccz-1]"
     (forall (p q)
      (if (has-occurrent-part p q)
@@ -169,7 +169,7 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
           (or (= tb ftp) (= tb ltp)))))))))
 
 
-  (cl:comment "b temporal part c (both spatiotemporal regions) iff b temporal projection is part of c's temporal projection, and for all parts of b's existence, if it spatially-projects-onto s at that time, then so does c [eom-1]"
+  (cl:comment "b temporal part c (both spatiotemporal regions) iff b temporal projection is part of c's temporal projection, and for all parts of b's existence, if it spatially-projects-onto s at that time, then so does c [eom-2]"
     (forall (b c)
      (if
       (and (exists (t) (instance-of b spatiotemporal-region t))

src/common logic/order.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2022/09/23
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text

src/common logic/participation.cl

@@ -1,14 +1,14 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2021/11/12
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text
 
   (cl:ttl https://basic-formal-ontology.org/2020/formulas/clif/participation.cl
 
-   (cl:outdiscourse exists-at occurrent-part-of concretizes specifically-depends-on temporal-part-of instance-of has-participant participates-in)
+   (cl:outdiscourse exists-at occurrent-part-of concretizes specifically-depends-on occupies-temporal-region temporal-part-of instance-of has-participant participates-in)
 
   (cl:comment "participates-in and has-participant are inverse relations [xjr-1]"
     (forall (t a b) (iff (participates-in a b t) (has-participant b a t))))
@@ -25,6 +25,12 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
       (participates-in p q s))))
 
 
+  (cl:comment "If c participates in p at t and p occupies-temporal-region r then t is part of r [kxe-1]"
+    (forall (c p r t)
+     (if (and (occupies-temporal-region p r) (participates-in c p t))
+      (temporal-part-of t r))))
+
+
   (cl:comment "participates-in is time indexed and has domain: independent-continuant but not spatial-region or specifically-dependent-continuant or generically-dependent-continuant  and range: process [ild-1]"
     (forall (a b t)
      (if (participates-in a b t)

src/common logic/spatial.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2021/11/12
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text
@@ -204,4 +204,4 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
             (and (not (= rprime r)) (continuant-part-of rprime r t2)
              (occupies-spatial-region c rprime t2)))))))))))
 
-)))
+)))

src/common logic/spatiotemporal.cl

@@ -1,7 +1,7 @@
 (cl:comment '
-BFO 2020 Axiomatization, generated 2021/11/12
+BFO 2020 Axiomatization, generated 2024/01/08
 The most current version of this file will always be at the GitHub repository https://github.com/bfo-ontology/bfo-2020
-Author: Alan Ruttenberg - alanruttenberg@gmail.com
+Author: Alan Ruttenberg - alanruttenberg(at)gmail.com
 This work is licensed under a Creative Commons "Attribution 4.0 International" license: https://creativecommons.org/licenses/by/4.0/'
 
  (cl:text
@@ -71,6 +71,21 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
         (temporally-projects-onto st t))))))
 
 
+  (cl:comment "temporally-projects-onto has domain spatiotemporal-region and range temporal-region [cvr-2]"
+    (forall (a b)
+     (if (temporally-projects-onto a b)
+      (and (exists (t) (instance-of a spatiotemporal-region t))
+       (instance-of b temporal-region b)))))
+
+
+  (cl:comment "If a occupies-spatial-region b then if a is an instance of material-entity then b is an instance of three-dimensional-spatial-region [ocw-1]"
+    (forall (p q t)
+     (if
+      (and (occupies-spatial-region p q t)
+       (instance-of p material-entity t))
+      (instance-of q three-dimensional-spatial-region t))))
+
+
   (cl:comment "A process boundary occupies a spatiotemporal instant [atz-1]"
     (forall (pb tr)
      (if
@@ -87,13 +102,6 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
       (exists (s) (occupies-spatiotemporal-region p s)))))
 
 
-  (cl:comment "temporally-projects-onto has domain spatiotemporal-region and range temporal-region [cvr-1]"
-    (forall (a b)
-     (if (temporally-projects-onto a b)
-      (and (exists (t) (instance-of a spatiotemporal-region t))
-       (exists (t) (instance-of b temporal-region t))))))
-
-
   (cl:comment "Spatiotemporal regions always project on to some temporal region [scq-1]"
     (forall (st)
      (if (exists (t) (instance-of st spatiotemporal-region t))
@@ -102,6 +110,14 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
         (temporally-projects-onto st t))))))
 
 
+  (cl:comment "Every temporal region is a projection from a spatiotemporal region [xco-2]"
+    (forall (tr)
+     (if (instance-of tr temporal-region tr)
+      (exists (st)
+       (and (exists (t) (instance-of st spatiotemporal-region t))
+        (temporally-projects-onto st tr))))))
+
+
   (cl:comment "spatially-projects-onto is time indexed and has domain: spatiotemporal-region and range: spatial-region [blj-1]"
     (forall (a b t)
      (if (spatially-projects-onto a b t)
@@ -110,12 +126,14 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
        (instance-of t temporal-region t)))))
 
 
-  (cl:comment "Every temporal region is a projection from a spatiotemporal region [xco-1]"
-    (forall (tr)
-     (if (exists (t) (instance-of tr temporal-region t))
-      (exists (st)
-       (and (exists (t) (instance-of st spatiotemporal-region t))
-        (temporally-projects-onto st tr))))))
+  (cl:comment "occupies-temporal-region has domain process or process-boundary  and range temporal-region [lyx-2]"
+    (forall (a b)
+     (if (occupies-temporal-region a b)
+      (and
+       (exists (t)
+        (or (instance-of a process t)
+         (instance-of a process-boundary t)))
+       (instance-of b temporal-region b)))))
 
 
   (cl:comment "Spatiotemporal regions always project on to some spatial region at any time [geq-1]"
@@ -126,16 +144,6 @@ This work is licensed under a Creative Commons "Attribution 4.0 International" l
         (spatially-projects-onto st s tp))))))
 
 
-  (cl:comment "occupies-temporal-region has domain process or process-boundary  and range temporal-region [lyx-1]"
-    (forall (a b)
-     (if (occupies-temporal-region a b)
-      (and
-       (exists (t)
-        (or (instance-of a process t)
-         (instance-of a process-boundary t)))
-       (exists (t) (instance-of b temporal-region t))))))
-
-
   (cl:comment "Every spatial region is a projection from a spatiotemporal region [mdb-1]"
     (forall (sr)
      (if (exists (t) (instance-of sr spatial-region t))