Skip to content
Permalink
Browse files

verification of occupy_root

  • Loading branch information...
gruninger committed Dec 15, 2017
1 parent 07da0ec commit 50fc9e63f9ab2c914a8bd166070dc47c32a673a4
Showing with 479 additions and 5 deletions.
  1. +32 −0 ontologies/occupy/occupy_connection/occupy_connection.clif
  2. +32 −0 ontologies/occupy/occupy_mereology/occupy_mereology.clif
  3. +5 −5 ontologies/occupy/occupy_root.clif
  4. +16 −0 ontologies/occupy/physical_connection/physical_connection.clif
  5. +22 −0 ontologies/occupy/physical_mereology/physical_mereology.clif
  6. +41 −0 ontologies/occupy/physical_mt/physical_mt.clif
  7. +10 −0 ontologies/occupy/region_connection/region_connection.clif
  8. +10 −0 ontologies/occupy/region_mereology/region_mereology.clif
  9. +15 −0 ontologies/occupy/region_mt/region_mt.clif
  10. +14 −0 ontologies/occupy/theorems/connection2region/Pi2.clif
  11. +28 −0 ontologies/occupy/theorems/graph_hom2occupy/Pi8.clif
  12. +14 −0 ontologies/occupy/theorems/graph_loops2physical/Pi5.clif
  13. +14 −0 ontologies/occupy/theorems/m_mereology2region/Pi1.clif
  14. +28 −0 ontologies/occupy/theorems/mapping_preserve2occupy/Pi7.clif
  15. +18 −0 ontologies/occupy/theorems/mereograph2physical/Pi6.clif
  16. +18 −0 ontologies/occupy/theorems/mt2region/Pi3.clif
  17. +28 −0 ontologies/occupy/theorems/occupy2graph_hom/Delta8.clif
  18. +28 −0 ontologies/occupy/theorems/occupy2mapping_preserve/Delta7.clif
  19. +14 −0 ontologies/occupy/theorems/partial_ordering2physical/Pi4.clif
  20. +14 −0 ontologies/occupy/theorems/physical2graph_loops/Delta5.clif
  21. +18 −0 ontologies/occupy/theorems/physical2mereograph/Delta6.clif
  22. +14 −0 ontologies/occupy/theorems/physical2partial_ordering/Delta4.clif
  23. +14 −0 ontologies/occupy/theorems/region2connection/Delta2.clif
  24. +14 −0 ontologies/occupy/theorems/region2m_mereology/Delta1.clif
  25. +18 −0 ontologies/occupy/theorems/region2mt/Delta3.clif
@@ -0,0 +1,32 @@
(cl-text http://colore.oor.net/occupy/occupy_connection/occupy_connection.clif

(cl-imports http://colore.oor.net/occupy/region_connection/region_connection.clif)

(cl-imports http://colore.oor.net/occupy/physical_connection/physical_connection.clif)

(forall (x)
(if (region x)
(not (physical_object x))))

(forall (x y)
(if (occupies x y)
(and (physical_object x)
(region y))))

(forall (x y z)
(if (and (occupies x y)
(occupies x z))
(= y z)))

(forall (x)
(if (physical_object x)
(exists (y)
(occupies x y))))

(forall (x y r1 r2)
(if (and (physical_C x y)
(occupies x r1)
(occupies y r2))
(C r1 r2)))

)
@@ -0,0 +1,32 @@
(cl-text http://colore.oor.net/occupy/occupy_mereology/occupy_mereology.clif

(cl-imports http://colore.oor.net/occupy/region_mereology/region_mereology.clif)

(cl-imports http://colore.oor.net/occupy/physical_mereology/physical_mereology.clif)

(forall (x)
(if (region x)
(not (physical_object x))))

(forall (x y)
(if (occupies x y)
(and (physical_object x)
(region y))))

(forall (x y z)
(if (and (occupies x y)
(occupies x z))
(= y z)))

(forall (x)
(if (physical_object x)
(exists (y)
(occupies x y))))

(forall (x y r1 r2)
(if (and (physical_part x y)
(occupies x r1)
(occupies y r2))
(part r1 r2)))

)
@@ -38,17 +38,17 @@

(forall (x)
(if (physical_object x)
(C x x)))
(physical_C x x)))

(forall (x y)
(if (C x y)
(C y x)))
(if (physical_C x y)
(physical_C y x)))

(forall (x y)
(if (physical_part x y)
(forall (z)
(if (physical_C x z)
(physical_C z y)))))
(if (physical_part y z)
(physical_C x z)))))

(forall (x)
(if (region x)
@@ -0,0 +1,16 @@
(cl-text http://colore.oor.net/occupy/physical_connection/physical_connection.clif

(forall (x y)
(if (physical_C x y)
(and (physical_object x)
(physical_object y))))

(forall (x)
(if (physical_object x)
(physical_C x x)))

(forall (x y)
(if (physical_C x y)
(physical_C y x)))

)
@@ -0,0 +1,22 @@
(cl-text http://colore.oor.net/occupy/physical_mereology/physical_mereology.clif

(forall (x y)
(if (physical_part x y)
(and (physical_object x)
(physical_object y))))

(forall (x)
(if (physical_object x)
(physical_part x x)))

(forall (x y)
(if (and (physical_part x y)
(physical_part y x))
(= x y)))

(forall (x y z)
(if (and (physical_part x y)
(physical_part y z))
(physical_part x z)))

)
@@ -0,0 +1,41 @@
(cl-text http://colore.oor.net/occupy/physical_mt/physical_mt.clif

(forall (x y)
(if (physical_part x y)
(and (physical_object x)
(physical_object y))))

(forall (x y)
(if (physical_C x y)
(and (physical_object x)
(physical_object y))))

(forall (x)
(if (physical_object x)
(physical_part x x)))

(forall (x y)
(if (and (physical_part x y)
(physical_part y x))
(= x y)))

(forall (x y z)
(if (and (physical_part x y)
(physical_part y z))
(physical_part x z)))

(forall (x)
(if (physical_object x)
(physical_C x x)))

(forall (x y)
(if (physical_C x y)
(physical_C y x)))

(forall (x y)
(if (physical_part x y)
(forall (z)
(if (physical_part y z)
(physical_C x z)))))

)
@@ -0,0 +1,10 @@
(cl-text http://colore.oor.net/occupy/region_connection/region_connection.clif

(cl-domain region (cl-imports http://colore.oor.net/mereotopology/connection.clif))

(forall (x y)
(if (C x y)
(and (region x)
(region y))))

)
@@ -0,0 +1,10 @@
(cl-text http://colore.oor.net/occupy/region_mereology/region_mereology.clif

(cl-domain region (cl-imports http://colore.oor.net/mereology/m_mereology.clif))

(forall (x y)
(if (part x y)
(and (region x)
(region y))))

)
@@ -0,0 +1,15 @@
(cl-text http://colore.oor.net/occupy/region_mt/region_mt.clif

(cl-domain region (cl-imports http://colore.oor.net/combined_mereotopology/mt.clif))

(forall (x y)
(if (part x y)
(and (region x)
(region y))))

(forall (x y)
(if (C x y)
(and (region x)
(region y))))

)
@@ -0,0 +1,14 @@

(cl-text http://colore.oor.net/occupy/theorems/connection2region/Pi2.clif

(cl-imports http://colore.oor.net/mereotopology/connection.clif)

(forall (x)
(iff (region x)
(= x x)))

(forall (x)
(iff (spatial_part x y)
(part x y)))

)
@@ -0,0 +1,28 @@

(cl-text http://colore.oor.net/occupy/theorems/graph_hom2occupy/Pi8.clif

(cl-imports http://colore.oor.net/occupy/subgraph/graph_hom.clif)

(forall (x)
(iff (physical_body x)
(point x)))

(forall (x)
(iff (region x)
(line x)))

(forall (x y)
(iff (spatial_C x y)
(C x y)))

(forall (x y)
(iff (physical_C x y)
(adj x y)))

(forall (x y)
(iff (occupies x y)
(and (in x y)
(point x)
(line y))))

)
@@ -0,0 +1,14 @@

(cl-text http://colore.oor.net/occupy/theorems/graph_loops2physical/Pi5.clif

(cl-imports http://colore.oor.net/graphs/graph_loops.clif)

(forall (x)
(iff (physical_body x)
(= x x)))

(forall (x)
(iff (physical_C x y)
(adj x y)))

)
@@ -0,0 +1,14 @@

(cl-text http://colore.oor.net/occupy/theorems/m_mereology2region/Pi1.clif

(cl-imports http://colore.oor.net/mereology/m_mereology.clif)

(forall (x)
(iff (region x)
(= x x)))

(forall (x)
(iff (spatial_part x y)
(part x y)))

)
@@ -0,0 +1,28 @@

(cl-text http://colore.oor.net/occupy/theorems/mapping_preserve2occupy/Pi7.clif

(cl-imports http://colore.oor.net/occupy/multigeometry/mapping_preserve.clif)

(forall (x)
(iff (physical_body x)
(point x)))

(forall (x)
(iff (region x)
(line x)))

(forall (x y)
(iff (spatial_part x y)
(part x y)))

(forall (x y)
(iff (physical_part x y)
(leq x y)))

(forall (x y)
(iff (occupies x y)
(and (in x y)
(point x)
(line y))))

)
@@ -0,0 +1,18 @@

(cl-text http://colore.oor.net/occupy/theorems/mereograph2physical/Pi6.clif

(cl-imports http://colore.oor.net/mereographs/mereograph.clif)

(forall (x)
(iff (physical_body x)
(= x x)))

(forall (x)
(iff (physical_part x y)
(leq x y)))

(forall (x)
(iff (physical_C x y)
(adj x y)))

)
@@ -0,0 +1,18 @@

(cl-text http://colore.oor.net/occupy/theorems/mt2region/Pi3.clif

(cl-imports http://colore.oor.net/combined_mereotopology/mt.clif)

(forall (x)
(iff (region x)
(= x x)))

(forall (x)
(iff (spatial_part x y)
(part x y)))

(forall (x)
(iff (spatial_C x y)
(C x y)))

)
@@ -0,0 +1,28 @@

(cl-text http://colore.oor.net/occupy/theorems/occupy2graph_hom/Delta8.clif

(cl-imports http://colore.oor.net/occupy/occupy_mereology/occupy_connection.clif)

(forall (x)
(iff (point x)
(physical_body x)))

(forall (x)
(iff (line x)
(region x)))

(forall (x y)
(iff (C x y)
(spatial_C x y)))

(forall (x y)
(iff (adj x y)
(physical_C x y)))

(forall (x y)
(iff (in x y)
(or (occupies x y)
(occupies y x)
(= x y))))

)
Oops, something went wrong.

0 comments on commit 50fc9e6

Please sign in to comment.
You can’t perform that action at this time.