Skip to content

Commit

Permalink
codi_down_atomic added
Browse files Browse the repository at this point in the history
  • Loading branch information
@thahmann
thahmann committed Apr 24, 2018
1 parent e8a07fa commit b023abd
Show file tree
Hide file tree
Showing 5 changed files with 105 additions and 16 deletions.
6 changes: 3 additions & 3 deletions ontologies/multidim_mereotopology_codi/conversions/codi_down.p9
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ formulas(sos).
% cl-imports multidim_mereotopology_codi/codi_int.clif
( all x12 all x11 ( (- (zex(difference(x12, x11)))) -> (eqdim(x12, difference(x12, x11))) )) .
( all x22 all x21 ( (lt(x21, x22)) -> ((x22=difference(x22, x21))) )) .
( all x32 all x31 all x33 ( ((leq(x32, x31) & cont(x33, x32) & lt(intersection(x33, x31), x33))) -> (cont(x33, difference(x32, x31))) )) .
( all x42 all x41 all x43 ( ((leq(x42, x41) & cont(x43, difference(x42, x41)))) -> (cont(x43, x42)) )) .
( all x52 all x51 all x53 ( ((leq(x52, x51) & p(x53, difference(x52, x51)))) -> (lt(intersection(x53, x51), x53)) )) .
( all x33 all x32 all x31 ( ((leq(x33, x32) & cont(x31, x33) & lt(intersection(x31, x32), x31))) -> (cont(x31, difference(x33, x32))) )) .
( all x43 all x42 all x41 ( ((leq(x43, x42) & cont(x41, difference(x43, x42)))) -> (cont(x41, x43)) )) .
( all x53 all x52 all x51 ( ((leq(x53, x52) & p(x51, difference(x53, x52)))) -> (lt(intersection(x51, x52), x51)) )) .
( all x62 all x61 ( (zex(difference(x62, x61))) <-> ((zex(x62) | cont(x62, x61))) )) .
end_of_list.
50 changes: 50 additions & 0 deletions ontologies/multidim_mereotopology_codi/conversions/codi_down_atomic.all.tptp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
fof(sos10,axiom,( ! [X12] : ! [X11] : ( (eqdim(X12, X11)) <=> ((leq(X12, X11) & leq(X11, X12))) )) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_mereotopology_dim/definitions/dim_basic_defs.clif
fof(sos20,axiom,( ! [X23] : ! [X22] : ( (covers(X23, X22)) <=> ((lt(X22, X23) & ( ! [X21] : ~ ((lt(X22, X21) & lt(X21, X23)))) )) )) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_mereotopology_dim/definitions/min_max_dim.clif
% cl-imports multidim_mereotopology_dim/definitions/covers.clif
% cl-imports multidim_mereotopology_codi/codi_down.clif
fof(sos30,axiom,( ! [X32] : ( (~ (zex(X32))) => (( ? [X31] : (p(X31, X32) & min(X31))) ) )) ).
% cl-imports multidim_mereotopology_codi/codi_int.clif
fof(sos40,axiom,( ! [X42] : ! [X41] : ( (~ (zex(difference(X42, X41)))) => (eqdim(X42, difference(X42, X41))) )) ).
fof(sos50,axiom,( ! [X52] : ! [X51] : ( (lt(X51, X52)) => ((X52=difference(X52, X51))) )) ).
fof(sos60,axiom,( ! [X63] : ! [X62] : ! [X61] : ( ((leq(X63, X62) & cont(X61, X63) & lt(intersection(X61, X62), X61))) => (cont(X61, difference(X63, X62))) )) ).
fof(sos70,axiom,( ! [X73] : ! [X72] : ! [X71] : ( ((leq(X73, X72) & cont(X71, difference(X73, X72)))) => (cont(X71, X73)) )) ).
fof(sos80,axiom,( ! [X83] : ! [X82] : ! [X81] : ( ((leq(X83, X82) & p(X81, difference(X83, X82)))) => (lt(intersection(X81, X82), X81)) )) ).
fof(sos90,axiom,( ! [X92] : ! [X91] : ( (zex(difference(X92, X91))) <=> ((zex(X92) | cont(X92, X91))) )) ).
% cl-imports multidim_mereotopology_cont/cont_basic.clif
% cl-imports multidim_mereotopology_cont/definitions/c.clif
% cl-imports multidim_mereotopology_dim/dim_prime_linear.clif
% cl-imports multidim_mereotopology_dim/definitions/dim_defs.clif
fof(sos100,axiom,( ! [X102] : ! [X101] : ( (cont(X102, X101)) => ((lt(X102, X101) | eqdim(X102, X101))) )) ).
fof(sos110,axiom,( ? [X111] : zex(X111)) ).
% cl-imports multidim_mereotopology_codi/codi_linear.clif
% cl-imports multidim_mereotopology_zex/zex.clif
fof(sos120,axiom,( ! [X122] : ! [X121] : ( (~ (c(X122, X121))) <=> (zex(intersection(X122, X121))) )) ).
fof(sos130,axiom,( ! [X132] : ! [X131] : ( (~ (zex(intersection(X132, X131)))) => (cont(intersection(X132, X131), X132)) )) ).
fof(sos140,axiom,( ! [X143] : ! [X142] : ! [X141] : ( ((cont(X141, X143) & cont(X141, X142))) => (leq(X141, intersection(X143, X142))) )) ).
fof(sos150,axiom,( ! [X153] : ! [X152] : ! [X151] : ( ((cont(X151, X153) & cont(X151, X152) & eqdim(X151, intersection(X153, X152)))) <=> (p(X151, intersection(X153, X152))) )) ).
% cl-imports multidim_mereotopology_cont/cont_basic.clif
fof(sos160,axiom,( ! [X163] : ! [X162] : ( (c(X163, X162)) <=> (( ? [X161] : (cont(X161, X163) & cont(X161, X162))) ) )) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_mereotopology_dim/definitions/min_max_dim.clif
fof(sos170,axiom,( ? [X171] : mindim(X171)) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
fof(sos180,axiom,( ! [X182] : ( (maxdim(X182)) <=> ((~ (zex(X182)) & ( ! [X181] : leq(X181, X182)) )) )) ).
fof(sos190,axiom,( ! [X192] : ( (mindim(X192)) <=> ((~ (zex(X192)) & ( ! [X191] : ( (~ (zex(X191))) => (leq(X192, X191)) )) )) )) ).
fof(sos200,axiom,( ! [X201] : leq(X201, X201)) ).
fof(sos210,axiom,( ! [X213] : ! [X212] : ! [X211] : ( ((leq(X213, X212) & leq(X212, X211))) => (leq(X213, X211)) )) ).
fof(sos220,axiom,( ! [X222] : ! [X221] : ( ((zex(X222) & zex(X221))) => ((X222=X221)) )) ).
fof(sos230,axiom,( ! [X232] : ! [X231] : ( (zex(X232)) => (leq(X232, X231)) )) ).
fof(sos240,axiom,( ! [X241] : ( (~ (zex(X241))) <=> (cont(X241, X241)) )) ).
fof(sos250,axiom,( ! [X252] : ! [X251] : ( ((cont(X252, X251) & cont(X251, X252))) => ((X252=X251)) )) ).
fof(sos260,axiom,( ! [X263] : ! [X262] : ! [X261] : ( ((cont(X263, X262) & cont(X262, X261))) => (cont(X263, X261)) )) ).
fof(sos270,axiom,( ! [X272] : ! [X271] : ( (zex(X272)) => ((~ (cont(X271, X272)) & ~ (cont(X272, X271)))) )) ).
fof(sos280,axiom,( ! [X282] : ! [X281] : ( ((zex(X282) & zex(X281))) => ((X282=X281)) )) ).
% cl-imports multidim_mereotopology_dim/definitions/eq_dim.clif
fof(sos290,axiom,( ! [X292] : ! [X291] : ( (gt(X292, X291)) <=> (lt(X291, X292)) )) ).
fof(sos300,axiom,( ! [X302] : ! [X301] : ( (geq(X302, X301)) <=> (leq(X301, X302)) )) ).
fof(sos310,axiom,( ! [X312] : ! [X311] : ( (lt(X312, X311)) <=> ((leq(X312, X311) & ~ (eqdim(X312, X311)))) )) ).
4 changes: 4 additions & 0 deletions ontologies/multidim_mereotopology_codi/conversions/codi_down_atomic.p9
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
formulas(sos).
% cl-imports multidim_mereotopology_codi/codi_down.clif
( all x12 ( (- (zex(x12))) -> (( exists x11 (p(x11, x12) & min(x11))) ) )) .
end_of_list.
42 changes: 42 additions & 0 deletions ontologies/multidim_mereotopology_codi/conversions/codi_int.all.tptp
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
fof(con,conjecture,(! [X243] : ! [X244] (zex(243) => (zex(intersection(X243, X244)))))).
% cl-imports multidim_mereotopology_codi/codi_linear.clif
% cl-imports multidim_mereotopology_zex/zex.clif
fof(sos10,axiom,( ! [X12] : ! [X11] : ( (~ (c(X12, X11))) <=> (zex(intersection(X12, X11))) )) ).
fof(sos20,axiom,( ! [X22] : ! [X21] : ( (~ (zex(intersection(X22, X21)))) => (cont(intersection(X22, X21), X22)) )) ).
fof(sos30,axiom,( ! [X32] : ! [X31] : ! [X33] : ( ((cont(X33, X32) & cont(X33, X31))) => (leq(X33, intersection(X32, X31))) )) ).
fof(sos40,axiom,( ! [X42] : ! [X41] : ! [X43] : ( ((cont(X43, X42) & cont(X43, X41) & eqdim(X43, intersection(X42, X41)))) <=> (p(X43, intersection(X42, X41))) )) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_mereotopology_dim/definitions/min_max_dim.clif
% cl-imports multidim_mereotopology_dim/definitions/covers.clif
fof(sos50,axiom,( ? [X51] : zex(X51)) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_mereotopology_dim/definitions/min_max_dim.clif
fof(sos60,axiom,( ? [X61] : mindim(X61)) ).
fof(sos70,axiom,( ! [X71] : ( (~ (zex(X71))) <=> (cont(X71, X71)) )) ).
fof(sos80,axiom,( ! [X82] : ! [X81] : ( ((cont(X82, X81) & cont(X81, X82))) => ((X82=X81)) )) ).
fof(sos90,axiom,( ! [X92] : ! [X91] : ! [X93] : ( ((cont(X92, X91) & cont(X91, X93))) => (cont(X92, X93)) )) ).
fof(sos100,axiom,( ! [X102] : ! [X101] : ( (zex(X102)) => ((~ (cont(X101, X102)) & ~ (cont(X102, X101)))) )) ).
fof(sos110,axiom,( ! [X112] : ! [X111] : ( ((zex(X112) & zex(X111))) => ((X112=X111)) )) ).
% cl-imports multidim_mereotopology_cont/cont_basic.clif
% cl-imports multidim_mereotopology_cont/definitions/c.clif
% cl-imports multidim_mereotopology_dim/dim_prime_linear.clif
% cl-imports multidim_mereotopology_dim/definitions/dim_defs.clif
fof(sos120,axiom,( ! [X122] : ! [X121] : ( (cont(X122, X121)) => ((lt(X122, X121) | eqdim(X122, X121))) )) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
% cl-imports multidim_mereotopology_dim/definitions/dim_basic_defs.clif
fof(sos130,axiom,( ! [X132] : ! [X131] : ( (covers(X132, X131)) <=> ((lt(X131, X132) & ( ! [X133] : ~ ((lt(X131, X133) & lt(X133, X132)))) )) )) ).
% cl-imports multidim_mereotopology_cont/cont_basic.clif
fof(sos140,axiom,( ! [X142] : ! [X141] : ( (c(X142, X141)) <=> (( ? [X143] : (cont(X143, X142) & cont(X143, X141))) ) )) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
fof(sos150,axiom,( ! [X152] : ( (maxdim(X152)) <=> ((~ (zex(X152)) & ( ! [X151] : leq(X151, X152)) )) )) ).
fof(sos160,axiom,( ! [X162] : ( (mindim(X162)) <=> ((~ (zex(X162)) & ( ! [X161] : ( (~ (zex(X161))) => (leq(X162, X161)) )) )) )) ).
% cl-imports multidim_mereotopology_dim/definitions/eq_dim.clif
fof(sos170,axiom,( ! [X172] : ! [X171] : ( (gt(X172, X171)) <=> (lt(X171, X172)) )) ).
fof(sos180,axiom,( ! [X182] : ! [X181] : ( (geq(X182, X181)) <=> (leq(X181, X182)) )) ).
fof(sos190,axiom,( ! [X192] : ! [X191] : ( (lt(X192, X191)) <=> ((leq(X192, X191) & ~ (eqdim(X192, X191)))) )) ).
fof(sos200,axiom,( ! [X201] : leq(X201, X201)) ).
fof(sos210,axiom,( ! [X212] : ! [X211] : ! [X213] : ( ((leq(X212, X211) & leq(X211, X213))) => (leq(X212, X213)) )) ).
fof(sos220,axiom,( ! [X222] : ! [X221] : ( ((zex(X222) & zex(X221))) => ((X222=X221)) )) ).
fof(sos230,axiom,( ! [X232] : ! [X231] : ( (zex(X232)) => (leq(X232, X231)) )) ).
% cl-imports multidim_mereotopology_dim/dim_prime_linear_unbounded.clif
fof(sos240,axiom,( ! [X242] : ! [X241] : ( (eqdim(X242, X241)) <=> ((leq(X242, X241) & leq(X241, X242))) )) ).
19 changes: 6 additions & 13 deletions ontologies/multidim_mereotopology_codi/conversions/codi_int.p9
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,8 @@
% Automatically generated from CL/KIF
formulas(sos).
% Module http://colore.oor.net/multidim_mereotopology_codi/codi_int.clif
%imports("http://colore.oor.net/multidim_mereotopology_codi/codi_linear.clif").
%imports("http://colore.oor.net/multidim_mereotopology_zex/zex.clif").
% 'Int-A1: disconnected entities have empty intersection'
all x all y ((-(C(x, y)) <-> ZEX(intersection(x, y)))).
% 'Int-A2: the intersection is contained in the intersecting entities (also ensures the intersection is of no greater dimension than necessary)'
all x all y ((-(ZEX(intersection(x, y))) -> Cont(intersection(x, y), x))).
% 'Int-A3: the intersection is of greatest possible dimension (determines the dimension of the intersection)'
all x all y all z ((Cont(z, x) & Cont(z, y) -> <=(z, intersection(x, y)))).
% 'Int-A4: the intersection contains everything of the greatest possible dimension (and whatever those things contain)'
all x all y all z ((Cont(z, x) & Cont(z, y) & EqDim(z, intersection(x, y)) <-> P(z, intersection(x, y)))).

% cl-imports multidim_mereotopology_codi/codi_linear.clif
% cl-imports multidim_mereotopology_zex/zex.clif
( all x12 all x11 ( (- (c(x12, x11))) <-> (zex(intersection(x12, x11))) )) .
( all x22 all x21 ( (- (zex(intersection(x22, x21)))) -> (cont(intersection(x22, x21), x22)) )) .
( all x33 all x32 all x31 ( ((cont(x31, x33) & cont(x31, x32))) -> (leq(x31, intersection(x33, x32))) )) .
( all x43 all x42 all x41 ( ((cont(x41, x43) & cont(x41, x42) & eqdim(x41, intersection(x43, x42)))) <-> (p(x41, intersection(x43, x42))) )) .
end_of_list.

0 comments on commit b023abd

Please sign in to comment.