Skip to content
Permalink
Browse files

missing imports added to p, inc, and sc

  • Loading branch information...
thahmann committed Nov 9, 2018
1 parent ba74032 commit 2c0b6429a7644d7c5ef63604dd8241021300227a
@@ -0,0 +1,3 @@
formulas(sos).
( exists x2 zex(x2)) .
end_of_list.
@@ -1,18 +1,16 @@
formulas(sos).
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_codi/definitions/ep.clif
% cl-imports multidim_space_dim/definitions/dim_basic_defs.clif
% cl-imports multidim_space_cont/definitions/c.clif
% cl-imports multidim_space_codi/definitions/po.clif
% cl-imports multidim_space_codi/definitions/inc.clif
% cl-imports multidim_space_codi/definitions/sc.clif
% cl-imports multidim_space_codi/definitions/min_max_in_dim.clif
( all x12 all x11 ( ((s(x12) & s(x11) & - (c(x12, x11)))) <-> (zex(intersection(x12, x11))) )) .
( all x22 all x21 ( ((s(x22) & s(x21) & - (zex(intersection(x22, x21))))) -> (cont(intersection(x22, x21), x22)) )) .
( all x32 all x31 all x33 ( ((cont(x33, x32) & cont(x33, x31))) -> (leq(x33, intersection(x32, x31))) )) .
( all x42 all x41 all x43 ( ((cont(x43, x42) & cont(x43, x41) & eqdim(x43, intersection(x42, x41)))) <-> (p(x43, intersection(x42, x41))) )) .
( all x52 all x51 ( ((s(x52) & s(x51) & - (zex(difference(x52, x51))))) -> (eqdim(x52, difference(x52, x51))) )) .
( all x62 all x61 ( (lt(x61, x62)) -> ((x62=difference(x62, x61))) )) .
( all x72 all x71 all x73 ( ((leq(x72, x71) & cont(x73, x72) & lt(intersection(x73, x71), x73))) -> (cont(x73, difference(x72, x71))) )) .
( all x82 all x81 all x83 ( ((leq(x82, x81) & cont(x83, difference(x82, x81)))) -> (cont(x83, x82)) )) .
( all x92 all x91 all x93 ( ((leq(x92, x91) & p(x93, difference(x92, x91)))) -> (lt(intersection(x93, x91), x93)) )) .
( all x102 all x101 ( (zex(difference(x102, x101))) <-> ((zex(x102) | cont(x102, x101))) )) .
( all x11 all x12 ( ((s(x11) & s(x12) & - (c(x11, x12)))) <-> (zex(intersection(x11, x12))) )) .
( all x21 all x22 ( ((s(x21) & s(x22) & - (zex(intersection(x21, x22))))) -> (cont(intersection(x21, x22), x21)) )) .
( all x32 all x33 all x31 ( ((cont(x31, x32) & cont(x31, x33))) -> (leq(x31, intersection(x32, x33))) )) .
( all x42 all x43 all x41 ( ((cont(x41, x42) & cont(x41, x43) & eqdim(x41, intersection(x42, x43)))) <-> (p(x41, intersection(x42, x43))) )) .
( all x51 all x52 ( ((s(x51) & s(x52) & - (zex(difference(x51, x52))))) -> (eqdim(x51, difference(x51, x52))) )) .
( all x61 all x62 ( (lt(x62, x61)) -> ((x61=difference(x61, x62))) )) .
( all x72 all x73 all x71 ( ((leq(x72, x73) & cont(x71, x72) & lt(intersection(x71, x73), x71))) -> (cont(x71, difference(x72, x73))) )) .
( all x82 all x83 all x81 ( ((leq(x82, x83) & cont(x81, difference(x82, x83)))) -> (cont(x81, x82)) )) .
( all x92 all x93 all x91 ( ((leq(x92, x93) & p(x91, difference(x92, x93)))) -> (lt(intersection(x91, x93), x91)) )) .
( all x101 all x102 ( (zex(difference(x101, x102))) <-> ((zex(x101) | cont(x101, x102))) )) .
end_of_list.
@@ -1,7 +1,7 @@
formulas(sos).
% cl-imports multidim_space_codi/codi_down.clif
( all x12 all x11 (sum(x12, x11)=sum(x11, x12))) .
( all x22 all x21 ( (lt(x22, x21)) -> ((x21=sum(x22, x21))) )) .
( all x32 all x31 all x33 ( ((leq(x32, x31) & cont(x33, x31))) -> (cont(x33, sum(x32, x31))) )) .
( all x42 all x41 all x43 ( ((cont(x43, sum(x42, x41)) & - (cont(x43, x42)))) -> (cont(difference(x43, x42), x41)) )) .
( all x11 all x12 (sum(x11, x12)=sum(x12, x11))) .
( all x21 all x22 ( (lt(x21, x22)) -> ((x22=sum(x21, x22))) )) .
( all x32 all x33 all x31 ( ((leq(x32, x33) & cont(x31, x33))) -> (cont(x31, sum(x32, x33))) )) .
( all x42 all x43 all x41 ( ((cont(x41, sum(x42, x43)) & - (cont(x41, x42)))) -> (cont(difference(x41, x42), x43)) )) .
end_of_list.
@@ -2,5 +2,5 @@ formulas(sos).
% cl-imports multidim_space_codi/codi_down.clif
% cl-imports multidim_space_codi/definitions/epp.clif
% cl-imports multidim_space_codi/definitions/sc.clif
( all x12 ( (con(x12)) <-> ((s(x12) & ( all x11 ( (pp(x11, x12)) -> (sc(x11, difference(x12, x11))) )) )) )) .
( all x11 ( (con(x11)) <-> ((s(x11) & ( all x12 ( (pp(x12, x11)) -> (sc(x12, difference(x11, x12))) )) )) )) .
end_of_list.
@@ -1,4 +1,5 @@
formulas(sos).
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_dim/definitions/eq_dim.clif
( all x11 all x12 ( (p(x11, x12)) <-> ((cont(x11, x12) & eqdim(x11, x12))) )) .
end_of_list.
@@ -1,11 +1,7 @@
formulas(sos).
% cl-imports multidim_space_codi/codi_down.clif
% cl-imports multidim_space_codi/definitions/min_max_in_dim.clif
% cl-imports multidim_space_codi/definitions/connected.clif
% cl-imports multidim_space_codi/definitions/epp.clif
% cl-imports multidim_space_codi/definitions/sc.clif
% cl-imports multidim_space_dim/definitions/covers.clif
( all x12 ( (icon(x12)) <-> ((con(x12) & ( all x11 ( (pp(x11, x12)) -> (covers(x12, intersection(x11, difference(x12, x11)))) )) )) )) .
( all x22 ( (ucon(x22)) <-> ((con(x22) & ( all x21 all x23 ( ((pp(x21, x22) & cont(x23, x21) & cont(x23, difference(x22, x21)))) -> (cont(x23, intersection(x21, difference(x22, x21)))) )) )) )) .
( all x32 all x31 ( (strongc(x32, x31)) <-> ((sc(x32, x31) & eqdim(x32, x31) & covers(x32, intersection(x32, x31)))) )) .
( all x11 ( (icon(x11)) <-> ((con(x11) & ( all x12 ( (pp(x12, x11)) -> (covers(x11, intersection(x12, difference(x11, x12)))) )) )) )) .
end_of_list.
@@ -1,5 +1,5 @@
formulas(sos).
% cl-imports multidim_space_codi/codi_basic.clif
% cl-imports multidim_space_codi/definitions/ep.clif
( all x12 all x13 ( (inc(x12, x13)) <-> ((( exists x11 (lt(x11, x12) & cont(x11, x12) & p(x11, x13))) | ( exists x11 (lt(x11, x13) & cont(x11, x13) & p(x11, x12))) )) )) .
( all x12 all x13 ( (inc(x12, x13)) <-> ((( exists x11 (leq(x11, x12) & - (eqdim(x11, x12)) & cont(x11, x12) & p(x11, x13))) | ( exists x11 (leq(x11, x13) & - (eqdim(x11, x13)) & cont(x11, x13) & p(x11, x12))) )) )) .
end_of_list.
@@ -1,4 +1,5 @@
formulas(sos).
% cl-imports multidim_space_codi/codi_basic.clif
( all x12 all x13 ( (sc(x12, x13)) <-> ((( exists x11 (cont(x11, x12) & cont(x11, x13))) & ( all x11 ( ((cont(x11, x12) & cont(x11, x13))) -> ((lt(x11, x12) & lt(x11, x13))) )) )) )) .
% cl-imports multidim_space_dim/definitions/eq_dim.clif
( all x12 all x13 ( (sc(x12, x13)) <-> ((( exists x11 (cont(x11, x12) & cont(x11, x13))) & ( all x11 ( ((cont(x11, x12) & cont(x11, x13))) -> ((leq(x11, x12) & - (eqdim(x11, x12)) & leq(x11, x13) & - (eqdim(x11, x13)))) )) )) )) .
end_of_list.
@@ -0,0 +1,6 @@
formulas(sos).
% cl-imports multidim_space_codi/codi_down.clif
% cl-imports multidim_space_codi/definitions/sc.clif
% cl-imports multidim_space_dim/definitions/covers.clif
( all x11 all x12 ( (strongc(x11, x12)) <-> ((sc(x11, x12) & eqdim(x11, x12) & covers(x11, intersection(x11, x12)))) )) .
end_of_list.
@@ -23,6 +23,7 @@
(iff
(Curve x)
(and
(not (ZEX x))
(not (MinDim x))
(forall (y)
(iff
@@ -13,6 +13,8 @@

(cl-imports http://colore.oor.net/multidim_space_codi/codi_basic.clif)

(cl-imports http://colore.oor.net/multidim_space_dim/definitions/eq_dim.clif)

(cl-comment 'basic axioms of traditional parthood (parthood of equidimensional entities) which is a non-strict partial order')

(cl-comment 'parthood holds between two entities of the same spatial dimension')
@@ -23,10 +23,18 @@
(Inc x y)
(or
(exists (z)
(and (< z x) (Cont z x) (P z y))
(and (<= z x)
(not (EqDim z x))
(Cont z x)
(P z y)
)
)
(exists (z)
(and (< z y) (Cont z y) (P z x))
(and (<= z y)
(not (EqDim z y))
(Cont z y)
(P z x)
)
)
)
)
@@ -12,6 +12,8 @@

(cl-imports http://colore.oor.net/multidim_space_codi/codi_basic.clif)

(cl-imports http://colore.oor.net/multidim_space_dim/definitions/eq_dim.clif)

(cl-comment 'SC-D: superficial (weak) contact (contact is of a lesser dimension than either involved entity) - prover9 file needs extra parentheses')

(forall (x y)
@@ -31,8 +33,10 @@
(Cont z y)
)
(and
(< z x)
(< z y)
(<= z x)
(not (EqDim z x))
(<= z y)
(not (EqDim z y))
)
)
)
@@ -3,9 +3,9 @@ formulas(sos).
% cl-imports multidim_space_codi/definitions/ep.clif
% cl-imports multidim_space_codi/definitions/inc.clif
( all x11 - (inc(x11, x11))) .
( all x22 all x21 ( (inc(x22, x21)) -> (inc(x21, x22)) )) .
( all x32 all x31 ( (eqdim(x32, x31)) -> (- (inc(x32, x31))) )) .
( all x42 all x41 ( (inc(x42, x41)) -> ((lt(x42, x41) | lt(x41, x42))) )) .
( all x52 all x51 ( ((cont(x52, x51) & lt(x52, x51))) -> (inc(x52, x51)) )) .
( all x62 all x61 all x63 ( ((inc(x62, x61) & p(x61, x63))) -> (inc(x62, x63)) )) .
( all x21 all x22 ( (inc(x21, x22)) -> (inc(x22, x21)) )) .
( all x31 all x32 ( (eqdim(x31, x32)) -> (- (inc(x31, x32))) )) .
( all x41 all x42 ( (inc(x41, x42)) -> ((lt(x41, x42) | lt(x42, x41))) )) .
( all x51 all x52 ( ((cont(x51, x52) & lt(x51, x52))) -> (inc(x51, x52)) )) .
( all x62 all x63 all x61 ( ((inc(x62, x63) & p(x63, x61))) -> (inc(x62, x61)) )) .
end_of_list.
@@ -4,6 +4,6 @@ formulas(sos).
% cl-imports multidim_space_codi/definitions/ep.clif
% cl-imports multidim_space_codi/definitions/po.clif
( all x11 ( ((s(x11) & - (zex(x11)))) -> (po(x11, x11)) )) .
( all x22 all x21 ( (po(x22, x21)) -> (po(x21, x22)) )) .
( all x32 all x31 ( (po(x32, x31)) -> (eqdim(x32, x31)) )) .
( all x21 all x22 ( (po(x21, x22)) -> (po(x22, x21)) )) .
( all x31 all x32 ( (po(x31, x32)) -> (eqdim(x31, x32)) )) .
end_of_list.
@@ -3,11 +3,11 @@ formulas(sos).
% cl-imports multidim_space_cont/definitions/c.clif
% cl-imports multidim_space_codi/definitions/ep.clif
% cl-imports multidim_space_codi/definitions/sc.clif
( all x12 all x11 ( (sc(x12, x11)) -> (c(x12, x11)) )) .
( all x22 all x21 ( (sc(x22, x21)) -> (- (( exists x23 (cont(x23, x22) & p(x23, x21))) )) )) .
( all x32 all x31 ( (sc(x32, x31)) -> (- (( exists x33 (p(x33, x32) & cont(x33, x31))) )) )) .
( all x42 all x41 ( ((c(x42, x41) & ( all x43 (- (cont(x43, x42)) | - (cont(x43, x41)) | (- (p(x43, x42)) & - (p(x43, x41))))) )) -> (sc(x42, x41)) )) .
( all x11 all x12 ( (sc(x11, x12)) -> (c(x11, x12)) )) .
( all x22 all x23 ( (sc(x22, x23)) -> (- (( exists x21 (cont(x21, x22) & p(x21, x23))) )) )) .
( all x32 all x33 ( (sc(x32, x33)) -> (- (( exists x31 (p(x31, x32) & cont(x31, x33))) )) )) .
( all x42 all x43 ( ((c(x42, x43) & ( all x41 (- (cont(x41, x42)) | - (cont(x41, x43)) | (- (p(x41, x42)) & - (p(x41, x43))))) )) -> (sc(x42, x43)) )) .
( all x51 - (sc(x51, x51))) .
( all x62 all x61 ( (sc(x62, x61)) -> (sc(x61, x62)) )) .
( all x72 all x71 ( (sc(x72, x71)) -> (( exists x73 (lt(x73, x72) & lt(x73, x71) & cont(x73, x72) & cont(x73, x71))) ) )) .
( all x61 all x62 ( (sc(x61, x62)) -> (sc(x62, x61)) )) .
( all x72 all x73 ( (sc(x72, x73)) -> (( exists x71 (lt(x71, x72) & lt(x71, x73) & cont(x71, x72) & cont(x71, x73))) ) )) .
end_of_list.
@@ -0,0 +1,17 @@
formulas(sos).
% cl-imports multidim_space_voids/voids_extended.clif
( all x11 all x12 ( (hostsh(x11, x12)) <-> ((hostsv(x11, x12) & icon(r(x11)))) )) .
( all x21 all x22 ( (hostsg(x21, x22)) <-> ((hostsv(x21, x22) & - (icon(r(x21))))) )) .
( all x32 ( (hole(x32)) <-> (( exists x31 hostsh(x31, x32)) ) )) .
( all x42 ( (gap(x42)) <-> (( exists x41 hostsg(x41, x42)) ) )) .
( all x51 all x52 ( (hostscavity(x51, x52)) <-> ((hostsv(x51, x52) & - (covers(r(x51), op(x51, x52))))) )) .
( all x62 ( (cavity(x62)) <-> (( exists x61 hostscavity(x61, x62)) ) )) .
( all x71 all x72 ( (hostscavityi(x71, x72)) <-> ((hostscavity(x71, x72) & zex(op(x71, x72)))) )) .
( all x81 all x82 ( (hostscavityt(x81, x82)) <-> ((hostscavity(x81, x82) & - (zex(op(x81, x82))))) )) .
( all x91 all x92 ( (hostshollow(x91, x92)) <-> ((hostsv(x91, x92) & covers(r(x91), op(x91, x92)) & icon(op(x91, x92)))) )) .
( all x102 ( (hol(x102)) <-> (( exists x101 hostshollow(x101, x102)) ) )) .
( all x111 all x112 ( (hoststunnel(x111, x112)) <-> ((hostsv(x111, x112) & covers(r(x111), op(x111, x112)) & - (icon(op(x111, x112))))) )) .
( all x122 ( (tun(x122)) <-> (( exists x121 hoststunnel(x121, x122)) ) )) .
( all x132 all x134 ( (hostsve(x132, x134)) <-> ((hostsv(x132, x134) & ( exists x131 (p(x131, op(x132, x134)) & ( all x133 ( ((hostsv(x132, x133) & eqdim(intersection(x131, r(x133)), x131))) -> ((po(r(x134), r(x133)) & cont(intersection(x131, r(x133)), op(x132, x133)))) )) )) )) )) .
( all x141 all x142 ( (hostsvi(x141, x142)) <-> ((hostsv(x141, x142) & - (hostsve(x141, x142)))) )) .
end_of_list.

0 comments on commit 2c0b642

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