Merge branch 'release-2024-01-10'

BFO-ontology · Jan 30, 2024 · 08f2f9d · 08f2f9d
2 parents 044490f + 1df1274
commit 08f2f9d
Show file tree

Hide file tree

Showing 43 changed files with 952 additions and 191 deletions.
diff --git a/documentation/axiomatization pdfs/continuant-mereology.pdf b/documentation/axiomatization pdfs/continuant-mereology.pdf
diff --git a/documentation/axiomatization pdfs/existence-instantiation.pdf b/documentation/axiomatization pdfs/existence-instantiation.pdf
diff --git a/documentation/axiomatization pdfs/generic-dependence.pdf b/documentation/axiomatization pdfs/generic-dependence.pdf
diff --git a/documentation/axiomatization pdfs/history.pdf b/documentation/axiomatization pdfs/history.pdf
diff --git a/documentation/axiomatization pdfs/material-entity.pdf b/documentation/axiomatization pdfs/material-entity.pdf
diff --git a/documentation/axiomatization pdfs/occurrent-mereology.pdf b/documentation/axiomatization pdfs/occurrent-mereology.pdf
diff --git a/documentation/axiomatization pdfs/order.pdf b/documentation/axiomatization pdfs/order.pdf
diff --git a/documentation/axiomatization pdfs/participation.pdf b/documentation/axiomatization pdfs/participation.pdf
diff --git a/documentation/axiomatization pdfs/spatial.pdf b/documentation/axiomatization pdfs/spatial.pdf
diff --git a/documentation/axiomatization pdfs/spatiotemporal.pdf b/documentation/axiomatization pdfs/spatiotemporal.pdf
diff --git a/documentation/axiomatization pdfs/specific-dependency.pdf b/documentation/axiomatization pdfs/specific-dependency.pdf
diff --git a/documentation/axiomatization pdfs/temporal-region.pdf b/documentation/axiomatization pdfs/temporal-region.pdf
diff --git a/documentation/axiomatization pdfs/universal-declaration.pdf b/documentation/axiomatization pdfs/universal-declaration.pdf
diff --git a/documentation/temporal extensions/temporalized relations/temporalized-relations.pdf b/documentation/temporal extensions/temporalized relations/temporalized-relations.pdf
diff --git a/src/common logic/continuant-mereology.cl b/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

diff --git a/src/common logic/existence-instantiation.cl b/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

diff --git a/src/common logic/generic-dependence.cl b/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

diff --git a/src/common logic/history.cl b/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

diff --git a/src/common logic/material-entity.cl b/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

diff --git a/src/common logic/occurrent-mereology.cl b/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))

diff --git a/src/common logic/order.cl b/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

diff --git a/src/common logic/participation.cl b/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)