Skip to content

Commit

Permalink
renamed physcont to fullphyscont
Browse files Browse the repository at this point in the history
  • Loading branch information
@thahmann
thahmann committed Nov 9, 2018
1 parent 271affe commit 44875f9
Show file tree
Hide file tree
Showing 6 changed files with 54 additions and 56 deletions.
24 changes: 12 additions & 12 deletions ontologies/multidim_space_voids/conversions/voids.p9
View file
@@ -1,17 +1,17 @@
formulas(sos).
% cl-imports multidim_space_spch/spch_minimal.clif
% cl-imports multidim_space_ped/definitions/mat.clif
( all x12 all x11 ( (vs(x12, x11)) <-> ((ped(x12) & s(x11) & cont(x11, ch(x12)) & - (po(x11, r(x12))))) )) .
( all x22 all x21 ( (simplev(x21)) <-> ((icon(r(x21)) & ( exists x22 hostsv(x22, x21)) )) )) .
( all x32 all x31 ( (complexv(x31)) <-> ((- (icon(r(x31))) & ( exists x32 hostsv(x32, x31)) )) )) .
( all x11 all x12 ( (vs(x11, x12)) <-> ((ped(x11) & s(x12) & cont(x12, ch(x11)) & - (po(x12, r(x11))))) )) .
( all x21 all x22 ( (simplev(x22)) <-> ((icon(r(x22)) & ( exists x21 hostsv(x21, x22)) )) )) .
( all x31 all x32 ( (complexv(x32)) <-> ((- (icon(r(x32))) & ( exists x31 hostsv(x31, x32)) )) )) .
( all x41 ( (v(x41)) <-> ((simplev(x41) | complexv(x41))) )) .
( all x52 all x51 ( (hostsv(x52, x51)) -> ((hosts(x52, x51) & vs(x52, r(x51)) & strongc(r(x52), r(x51)))) )) .
( all x62 all x61 all x63 ( ((hostsv(x62, x61) & complexv(x61) & po(r(x63), r(x61)))) -> (( exists x64 (hostsv(x62, x64) & simplev(x64) & po(r(x63), r(x64)))) ) )) .
( all x72 all x71 ( ((hosts(x72, x71) & v(x71))) -> (- (v(x72))) )) .
( all x82 all x81 ( ((hostsv(x82, x81) & rpf(x82))) -> (( exists x83 (hosts(x83, x82) & - (f(x83)) & hostsv(x83, x81))) ) )) .
( all x92 all x91 ( ((hostsv(x92, x91) & - (f(x92)))) -> (( exists x93 (hosts(x92, x93) & rpf(x93) & hostsv(x93, x91))) ) )) .
( all x102 all x101 all x103 ( ((hostsv(x102, x101) & hostsv(x102, x103) & po(r(x101), r(x103)))) -> ((cont(r(x101), r(x103)) | cont(r(x103), r(x101)))) )) .
( all x112 all x111 all x114 ( ((hostsv(x112, x114) & p(r(x112), r(x111)) & ped(x111) & - (dpf(x111)) & - (cont(r(x114), r(x111))))) -> (( exists x113 (cont(difference(r(x114), r(x111)), r(x113)) & hostsv(x111, x113))) ) )) .
( all x122 all x121 all x124 ( ((hostsv(x122, x124) & p(r(x121), r(x122)) & ped(x121) & - (dpf(x121)) & po(r(x124), ch(x121)))) -> (( exists x123 ((r(x123)=intersection(r(x124), ch(x121))) & hostsv(x121, x123))) ) )) .
( all x132 all x131 all x133 ( ((mat(x131) & mat(x133) & hostsv(x131, x132) & p(r(x131), r(x133)) & - (po(r(x133), r(x132))))) -> (hostsv(x133, x132)) )) .
( all x51 all x52 ( (hostsv(x51, x52)) -> ((hosts(x51, x52) & vs(x51, r(x52)) & strongc(r(x51), r(x52)))) )) .
( all x62 all x64 all x61 ( ((hostsv(x62, x64) & complexv(x64) & po(r(x61), r(x64)))) -> (( exists x63 (hostsv(x62, x63) & simplev(x63) & po(r(x61), r(x63)))) ) )) .
( all x71 all x72 ( ((hosts(x71, x72) & v(x72))) -> (- (v(x71))) )) .
( all x82 all x83 ( ((hostsv(x82, x83) & rpf(x82))) -> (( exists x81 (hosts(x81, x82) & - (f(x81)) & hostsv(x81, x83))) ) )) .
( all x92 all x93 ( ((hostsv(x92, x93) & - (f(x92)))) -> (( exists x91 (hosts(x92, x91) & rpf(x91) & hostsv(x91, x93))) ) )) .
( all x102 all x103 all x101 ( ((hostsv(x102, x103) & hostsv(x102, x101) & po(r(x103), r(x101)))) -> ((cont(r(x103), r(x101)) | cont(r(x101), r(x103)))) )) .
( all x111 all x114 all x113 ( ((hostsv(x111, x113) & p(r(x111), r(x114)) & ped(x114) & - (dpf(x114)) & - (cont(r(x113), r(x114))))) -> (( exists x112 (cont(difference(r(x113), r(x114)), r(x112)) & hostsv(x114, x112))) ) )) .
( all x121 all x124 all x123 ( ((hostsv(x121, x123) & p(r(x124), r(x121)) & ped(x124) & - (dpf(x124)) & po(r(x123), ch(x124)))) -> (( exists x122 ((r(x122)=intersection(r(x123), ch(x124))) & hostsv(x124, x122))) ) )) .
( all x132 all x133 all x131 ( ((mat(x133) & mat(x131) & hostsv(x133, x132) & p(r(x133), r(x131)) & - (po(r(x131), r(x132))))) -> (hostsv(x131, x132)) )) .
end_of_list.
12 changes: 6 additions & 6 deletions ontologies/multidim_space_voids/conversions/voids_extended.p9
View file
@@ -1,10 +1,10 @@
formulas(sos).
% cl-imports multidim_space_voids/voids_opening.clif
% cl-imports multidim_space_space/space_dk1.clif
( all x14 all x13 ( (po(x14, porespace(x13))) <-> (( exists x12 (dk1(x12, x13) & ( all x11 ( (hostsv(x13, x11)) -> (- (po(x14, r(x11)))) )) & ( exists x11 (hostsv(x12, x11) & po(x14, r(x11)))) )) ) )) .
( all x23 all x22 ( (po(x23, voidspace(x22))) <-> ((po(x23, porespace(x22)) | ( exists x21 (hostsv(x22, x21) & po(x23, r(x21)))) )) )) .
( all x32 ( (- (zex(porespace(x32)))) -> (( exists x33 exists x31 ((r(x33)=porespace(x32)) & hostsv(x31, x33) & dk1(x31, x32))) ) )) .
( all x42 ( (- (zex(voidspace(x42)))) -> (( exists x43 exists x41 ((r(x43)=voidspace(x42)) & hostsv(x41, x43) & dk1(x41, x42))) ) )) .
( all x53 all x52 ( (po(x53, convoidspace(x52))) <-> (( exists x51 (po(x53, x51) & icon(x51) & cont(x51, voidspace(x52)) & strongc(x51, difference(cuni, sum(r(x52), voidspace(x52)))))) ) )) .
( all x63 all x62 ( (po(x63, conporespace(x62))) <-> (( exists x61 (po(x63, x61) & icon(x61) & cont(x61, porespace(x62)) & strongc(x61, difference(cuni, sum(r(x62), porespace(x62)))))) ) )) .
( all x13 all x14 ( (po(x13, porespace(x14))) <-> (( exists x11 (dk1(x11, x14) & ( all x12 ( (hostsv(x14, x12)) -> (- (po(x13, r(x12)))) )) & ( exists x12 (hostsv(x11, x12) & po(x13, r(x12)))) )) ) )) .
( all x22 all x23 ( (po(x22, voidspace(x23))) <-> ((po(x22, porespace(x23)) | ( exists x21 (hostsv(x23, x21) & po(x22, r(x21)))) )) )) .
( all x33 ( (- (zex(porespace(x33)))) -> (( exists x32 exists x31 ((r(x32)=porespace(x33)) & hostsv(x31, x32) & dk1(x31, x33))) ) )) .
( all x43 ( (- (zex(voidspace(x43)))) -> (( exists x42 exists x41 ((r(x42)=voidspace(x43)) & hostsv(x41, x42) & dk1(x41, x43))) ) )) .
( all x52 all x53 ( (po(x52, convoidspace(x53))) <-> (( exists x51 (po(x52, x51) & icon(x51) & cont(x51, voidspace(x53)) & strongc(x51, difference(cuni, sum(r(x53), voidspace(x53)))))) ) )) .
( all x62 all x63 ( (po(x62, conporespace(x63))) <-> (( exists x61 (po(x62, x61) & icon(x61) & cont(x61, porespace(x63)) & strongc(x61, difference(cuni, sum(r(x63), porespace(x63)))))) ) )) .
end_of_list.
4 changes: 1 addition & 3 deletions ontologies/multidim_space_voids/conversions/voids_extended_multigran.p9
View file
@@ -1,6 +1,4 @@
formulas(sos).
% cl-imports multidim_space_voids/voids_extended.clif
( all x12 all x11 ( (hostsv-any(x11, x12)) <-> ((hostsv(x11, x12) | hostsv-1(x11, x12) | hostsv-2(x11, x12) | hostsv-3(x11, x12))) )) .
( all x22 all x21 ( (po(x21, voidspace-all(x22))) <-> (( exists x23 (hostsv-any(x22, x23) & po(x21, r(x23)))) ) )) .
( all x32 ( ((mat(x32) & - (zex(voidspace-all(x32))))) -> (( exists x31 exists x33 ((r(x31)=voidspace-all(x32)) & hostsv(x33, x31))) ) )) .
% cl-imports multidim_space_voids/voids_multigran.clif
end_of_list.
6 changes: 3 additions & 3 deletions ontologies/multidim_space_voids/conversions/voids_multigran.p9
View file
@@ -1,6 +1,6 @@
formulas(sos).
% cl-imports multidim_space_voids/voids.clif
( all x12 all x11 ( (hostsvany(x11, x12)) <-> ((hostsv(x11, x12) | hostsv1(x11, x12) | hostsv2(x11, x12) | hostsv3(x11, x12))) )) .
( all x22 all x21 ( (po(x21, voidspaceall(x22))) <-> (( exists x23 (hostsvany(x22, x23) & po(x21, r(x23)))) ) )) .
( all x32 ( ((mat(x32) & - (zex(voidspaceall(x32))))) -> (( exists x31 exists x33 ((r(x31)=voidspaceall(x32)) & hostsv(x33, x31))) ) )) .
( all x11 all x12 ( (hostsvany(x12, x11)) <-> ((hostsv(x12, x11) | hostsv1(x12, x11) | hostsv2(x12, x11) | hostsv3(x12, x11))) )) .
( all x21 all x23 ( (po(x23, voidspaceall(x21))) <-> (( exists x22 (hostsvany(x21, x22) & po(x23, r(x22)))) ) )) .
( all x31 ( ((mat(x31) & - (zex(voidspaceall(x31))))) -> (( exists x33 exists x32 ((r(x33)=voidspaceall(x31)) & hostsv(x32, x33))) ) )) .
end_of_list.
2 changes: 1 addition & 1 deletion ontologies/multidim_space_voids/definitions/conversions/physcont.p9
View file
@@ -1,4 +1,4 @@
formulas(sos).
% cl-imports multidim_space_voids/voids_extended.clif
( all x12 all x11 ( (fully-phys-contains(x11, x12)) <-> ((ped(x12) & ped(x11) & p(r(x12), ch(x11)) & ( (- (mat(x11))) -> (p(r(x12), r(x11))) ))) )) .
( all x11 all x12 ( (fully-phys-contains(x12, x11)) <-> ((ped(x11) & ped(x12) & p(r(x11), ch(x12)) & ( (- (mat(x12))) -> (p(r(x11), r(x12))) ))) )) .
end_of_list.
62 changes: 31 additions & 31 deletions ...dim_space_voids/definitions/physcont.clif → ...space_voids/definitions/fullphyscont.clif
View file
@@ -1,32 +1,32 @@
/*******************************************************************************
* Copyright (c) University of Toronto and others. All rights reserved.
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 3.0 Unported license. The legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/3.0/legalcode.
*
* Contributors:
* Torsten Hahmann - initial implementation
*******************************************************************************/
(cl-text http://colore.oor.net/multidim_space_voids/definitions/physcont.clif
(cl-imports http://colore.oor.net/multidim_space_voids/voids_extended.clif)
(cl-comment 'FPCont-D: for x to be generically fully physically contained in y, both x and y must be physical endurants and the region of x must be within the convex hull of y and, if y is immaterial, within the region of y')
(forall (x y)
(iff
(fully-phys-contains y x)
(and
(PED x)
(PED y)
(P (r x) (ch y))
(if
(not (mat y))
(P (r x) (r y))
)
)
)
)
/*******************************************************************************
* Copyright (c) University of Toronto and others. All rights reserved.
* The content of this file is licensed under the Creative Commons Attribution-
* ShareAlike 3.0 Unported license. The legal text of this license can be
* found at http://creativecommons.org/licenses/by-sa/3.0/legalcode.
*
* Contributors:
* Torsten Hahmann - initial implementation
*******************************************************************************/

(cl-text http://colore.oor.net/multidim_space_voids/definitions/fullphyscont.clif

(cl-imports http://colore.oor.net/multidim_space_voids/voids_extended.clif)

(cl-comment 'FPCont-D: for x to be generically fully physically contained in y, both x and y must be physical endurants and the region of x must be within the convex hull of y and, if y is immaterial, within the region of y')

(forall (x y)
(iff
(fullphyscont y x)
(and
(PED x)
(PED y)
(P (r x) (ch y))
(if
(not (mat y))
(P (r x) (r y))
)
)
)
)

)

0 comments on commit 44875f9

Please sign in to comment.