Skip to content
Permalink
Browse files

corrected matter.clif and related theories

  • Loading branch information...
gruninger committed Feb 1, 2019
1 parent b95b747 commit 6795545850cef0d7418fe59280029d21589a6a1d
@@ -4,7 +4,7 @@

(forall (x y)
(if (constitutes x y)
(and (Matter x)
(and (mat x)
(MaterialObject x))))

(forall (x)
@@ -13,14 +13,14 @@
(constitutes y x))))

(forall (x y1 y2)
(if (and (Matter x)
(if (and (mat x)
(constitutes x y1)
(constitutes x y2))
(= y1 y2)))

(forall (x1 x2 y)
(if (and (Matter x1)
(Matter x2)
(if (and (mat x1)
(mat x2)
(constitutes x1 y)
(constitutes x2 y))
(= x1 x2)))
@@ -4,6 +4,10 @@

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

(forall (x)
(if (mat x)
(not (amount x))))

(forall (x)
(iff (mat x)
(amount (mass x))))
@@ -0,0 +1,43 @@
============================== prooftrans ============================
Prover9 (32) version Dec-2007, Dec 2007.
Process 38238 was started by mudcat on mie-16-81.internal.mie.utoronto.ca,
Fri Feb 1 14:53:53 2019
The command was "/Applications/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
============================== end of head ===========================

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.03 (+ 0.00) seconds.
% Length of proof is 23.
% Level of proof is 5.
% Maximum clause weight is 15.
% Given clauses 110.

2 (all x all y (chunkOf(x,y) & chunkOf(y,x) -> x = y)) # label(non_clause). [assumption].
5 (all x all y (chunk_overlaps(x,y) <-> (exists z (chunkOf(z,x) & chunkOf(z,y))))) # label(non_clause). [assumption].
12 (all x all y (mat(x) & mat(y) & -chunkOf(y,x) -> (exists z all u (chunkOf(u,z) <-> -chunk_overlaps(u,x))))) # label(non_clause). [assumption].
14 (all x all y (chunkOf(x,y) -> mat(x) & mat(y))) # label(non_clause). [assumption].
15 (all x (mat(x) -> -amount(x))) # label(non_clause). [assumption].
32 -(all x all y (mass(x) = mass(y) & x != y -> -chunkOf(x,y))) # label(non_clause). [assumption].
49 -chunkOf(x,y) | -chunkOf(y,x) | y = x. [clausify(2)].
54 -chunk_overlaps(x,y) | chunkOf(f1(x,y),x). [clausify(5)].
62 -mat(x) | -mat(y) | chunkOf(y,x) | chunkOf(z,f7(x,y)) | chunk_overlaps(z,x). [clausify(12)].
65 -chunkOf(x,y) | mat(x). [clausify(14)].
66 -chunkOf(x,y) | mat(y). [clausify(14)].
67 -mat(x) | -amount(x). [clausify(15)].
68 amount(Zero_mass). [assumption].
91 c3 != c2. [clausify(32)].
92 chunkOf(c2,c3). [clausify(32)].
140 -mat(Zero_mass). [ur(67,b,68,a)].
167 mat(c3). [resolve(92,a,66,a)].
168 mat(c2). [resolve(92,a,65,a)].
174 -chunkOf(c3,c2). [resolve(92,a,49,b),flip(b),unit_del(b,91)].
191 -chunkOf(x,Zero_mass). [ur(66,b,140,a)].
192 -chunkOf(Zero_mass,x). [ur(65,b,140,a)].
253 -chunk_overlaps(Zero_mass,x). [ur(54,b,191,a)].
332 $F. [ur(62,b,167,a,c,174,a,d,192,a,e,253,a),unit_del(a,168)].

============================== end of proof ==========================
@@ -0,0 +1,13 @@
(cl-text http://colore.oor.net/matter/definitions/chunk_diff.clif

(cl-imports http://colore.oor.net/matter/definitions/chunk_overlaps.clif)

(cl-comment 'Mereological difference for matter')
(forall (x y z)
(iff (chunk_diff x y z)
(forall (w)
(iff (chunkOf w z)
(and (chunkOf w x)
(not (chunk_overlaps w y)))))))

)
@@ -0,0 +1,12 @@
(cl-text http://colore.oor.net/matter/definitions/chunk_disjoint.clif

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

(cl-comment 'Disjointness for matter')
(forall (x y)
(iff (chunk_disjoint x y)
(and (mat x)
(mat y)
(not (chunk_overlaps x y)))))

)
@@ -0,0 +1,13 @@
(cl-text http://colore.oor.net/matter/definitions/chunk_overlaps.clif

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

(cl-comment 'Overlaps for matter')
(forall (x y)
(iff (chunk_overlaps x y)
(exists (z)
(and
(chunkOf z x)
(chunkOf z y)))))

)
@@ -0,0 +1,13 @@
(cl-text http://colore.oor.net/matter/definitions/chunk_underlaps.clif

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

(cl-comment 'Underlaps for matter')
(forall (x y)
(iff (chunk_underlaps x y)
(exists (z)
(and
(chunkOf x z)
(chunkOf y z)))))

)
@@ -0,0 +1,12 @@
(cl-text http://colore.oor.net/matter/definitions/proper_chunk.clif

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

(cl-comment 'Proper Parthood for matter')
(forall (x y)
(iff (proper_chunk x y)
(and (chunkOf x y)
(not (= x y)))))

)

@@ -1,38 +1,58 @@
(cl-text http://colore.oor.net/matter/matter.clif

(cl-comment 'Proper Parthood')
(forall (x y)
(iff (properChunkOf x y)
(and (chunkOf x y)
(not (= x y)))))

(cl-comment 'Overlaps')
(forall (x y)
(if (exists (z)
(and
(chunkOf z x)
(chunkOf z y)))
(chunkOverlaps x y)))

(cl-comment 'Disjointness')
(forall (x y)
(iff (chunkDisjoints x y)
(not (chunkOverlaps x y))))
(if (chunkOf x y)
(and (mat x)
(mat y))))

(cl-comment 'Transitivity')
(forall (x y z)
(if (and (chunkOf x y)
(chunkOf y z))
(chunkOf x z)))

(cl-comment 'Reflexivity')
(forall (x)
(chunkOf x x))
(if (mat x)
(chunkOf x x)))

(cl-comment 'Antisymmetry')
(forall (x y)
(if (and (chunkOf x y)
(chunkOf y x))
(= x y)))

(cl-comment 'Transitivity')
(forall (x y z)
(if (and (chunkOf x y)
(chunkOf y z))
(chunkOf x z)))

(forall (x y)
(if (and (mat x)
(mat y)
(not (chunkOf x y)))
(exists (z)
(and (chunkOf z x)
(chunk_disjoint z y)))))

(forall (x y)
(if (chunk_underlaps x y)
(exists (z)
(forall (v)
(iff (chunk_overlaps v z)
(or (chunk_overlaps v x)
(chunk_overlaps v y)))))))

(forall (x y)
(if (chunk_overlaps x y)
(exists (z)
(forall (v)
(iff (proper_chunk v z)
(or (proper_chunk v x)
(proper_chunk v y)))))))

(forall (x w)
(if (and (mat x)
(mat w)
(not (chunkOf w x)))
(exists (z)
(forall (y)
(iff (chunkOf y z)
(not (chunk_overlaps y x)))))))

)

0 comments on commit 6795545

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