Skip to content
Permalink
Browse files

CODI: existential extensions for proving nontrivial consistency

  • Loading branch information...
thahmann committed Apr 24, 2018
1 parent b023abd commit 55bb61a950c1ce698936d59fb842996861498275
Showing with 3,031 additions and 0 deletions.
  1. +241 −0 ontologies/multidim_mereotopology_codi/consistency/codi_down_all_nontrivial.clif
  2. +257 −0 ontologies/multidim_mereotopology_codi/consistency/codi_down_atomic_all_nontrivial.clif
  3. +339 −0 ontologies/multidim_mereotopology_codi/consistency/codi_down_sum_all_nontrivial.clif
  4. +421 −0 ontologies/multidim_mereotopology_codi/consistency/codi_updown_3d_all_nontrivial.clif
  5. +7 −0 ontologies/multidim_mereotopology_codi/consistency/codi_updown_3d_nontrivial.clif
  6. +75 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_down_all_nontrivial.all.tptp
  7. +29 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_down_all_nontrivial.p9
  8. +79 −0 ...gies/multidim_mereotopology_codi/consistency/conversions/codi_down_atomic_all_nontrivial.all.tptp
  9. +31 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_down_atomic_all_nontrivial.p9
  10. +129 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_down_sum_all_nontrivial.all.tptp
  11. +41 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_down_sum_all_nontrivial.p9
  12. +101 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_down_sum_nontrivial.all.tptp
  13. +13 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_down_sum_nontrivial.p9
  14. +185 −0 ...logies/multidim_mereotopology_codi/consistency/conversions/codi_updown_3d_all_nontrivial.all.tptp
  15. +50 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_updown_3d_all_nontrivial.p9
  16. +138 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_updown_3d_nontrivial.all.tptp
  17. +3 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_updown_3d_nontrivial.p9
  18. +97 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_updown_nontrivial.all.tptp
  19. +7 −0 ontologies/multidim_mereotopology_codi/consistency/conversions/codi_updown_nontrivial.p9
  20. +61 −0 ontologies/multidim_mereotopology_codi/theorems/consistency/codi_down_theoremsep-e1_nontrivial.clif
  21. +95 −0 ontologies/multidim_mereotopology_codi/theorems/consistency/codi_down_theoremsep-e2_nontrivial.clif
  22. +59 −0 ontologies/multidim_mereotopology_codi/theorems/consistency/codi_down_theoremspo-e1_nontrivial.clif
  23. +70 −0 ...m_mereotopology_codi/theorems/consistency/conversions/codi_down_theoremsep-e1_nontrivial.all.tptp
  24. +9 −0 ...ultidim_mereotopology_codi/theorems/consistency/conversions/codi_down_theoremsep-e1_nontrivial.p9
  25. +79 −0 ...m_mereotopology_codi/theorems/consistency/conversions/codi_down_theoremsep-e2_nontrivial.all.tptp
  26. +13 −0 ...ultidim_mereotopology_codi/theorems/consistency/conversions/codi_down_theoremsep-e2_nontrivial.p9
  27. +91 −0 ...m_mereotopology_codi/theorems/consistency/conversions/codi_down_theoremspo-e1_nontrivial.all.tptp
  28. +9 −0 ...ultidim_mereotopology_codi/theorems/consistency/conversions/codi_down_theoremspo-e1_nontrivial.p9
  29. +127 −0 ontologies/multidim_mereotopology_codi_length/consistency/codi_down_length_nontrivial.clif
  30. +120 −0 ...s/multidim_mereotopology_codi_length/consistency/conversions/codi_down_length_nontrivial.all.tptp
  31. +17 −0 ontologies/multidim_mereotopology_codi_length/consistency/conversions/codi_down_length_nontrivial.p9
  32. +28 −0 ...m_mereotopology_dim/consistency/conversions/dim_prime_linear_bounded_discrete_nontrivial.all.tptp
  33. +3 −0 ...ultidim_mereotopology_dim/consistency/conversions/dim_prime_linear_bounded_discrete_nontrivial.p9
  34. +7 −0 ontologies/multidim_mereotopology_dim/consistency/dim_prime_linear_bounded_discrete_nontrivial.clif
@@ -0,0 +1,241 @@
/** AUTOMATICALLY CREATED BY MACLEOD ON Tue Apr 24 10:53:33 2018**/

(cl-text multidim_mereotopology_codi\consistency\codi_down_all_nontrivial.clif

(cl-imports multidim_mereotopology_codi\codi_down.clif)

(exists (X0 X1)
(and
(Covers X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(Covers X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(<= X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(<= X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(> X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(> X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(Cont X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(Cont X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(C X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(C X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0)
(and
(ZEX X0)
)
)


(exists (X0)
(and
(not
(ZEX X0)
)
)
)


(exists (X0 X1 X2)
(and
(= (difference X0 X1) X2)
(not (= X0 X1))
(not (= X0 X2))
(not (= X1 X2))
)
)




(exists (X0)
(and
(MaxDim X0)
)
)


(exists (X0)
(and
(not
(MaxDim X0)
)
)
)


(exists (X0 X1)
(and
(EqDim X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(EqDim X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(P X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(P X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0)
(and
(MinDim X0)
)
)


(exists (X0)
(and
(not
(MinDim X0)
)
)
)


(exists (X0 X1 X2)
(and
(= (intersection X0 X1) X2)
(not (= X0 X1))
(not (= X0 X2))
(not (= X1 X2))
)
)




(exists (X0 X1)
(and
(< X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(< X0 X1)
)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(>= X0 X1)
(not (= X0 X1))
)
)


(exists (X0 X1)
(and
(not
(>= X0 X1)
)
(not (= X0 X1))
)
)


)
Oops, something went wrong.

0 comments on commit 55bb61a

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