proper occurrent part of is not declared transitive

[alanruttenberg]

Reported by Stefan Schulz. It's declared transitive in the FOL, but in an oversight it wasn't on the list of transitive properties for which the OWL transitivity axiom was added.

[wceusters]

Reported by Stefan Schulz. It's declared transitive in the FOL, but in an oversight it wasn't on the list of transitive properties for which the OWL transitivity axiom was added.

Where is it in FOL, i.e. the ISO version? kad-1 declares it for occurrent-part-of with as consequence that if 'a pop b' and 'b pop c' only follows that 'a op c'.

[alanruttenberg]

Sorry, my mistake - it's declared to be a theorem in the source from which the CL is generated, which is where I looked, and theorems are not included in the common logic. If follows from the definition of proper-occurrent-part-of, transitivity of occurrent-part-of and antisymmetry of occurrent-part-of: okr-1, kad-1, and xlu-1

It isn't in the OWL because all the OWL assertions are generated from specs and then verified provable, and the list for which there should be transitive assertions inadvertently omitted proper-occurrent-part-of. I've fixed the source but not regenerated the OWL yet.

If the forward relation is transitive, then that the inverse is transitive is also a theorem.

[alanruttenberg]

I never trust myself to reason. Here's a transcript of what I did. First I ask to prove the transitivity. Then I ask for how it was proved, and it includes the antisymmetry. Then I try to prove it without transitivity. Then I ask for a model where the two axioms are true but the transitivity isn't.

>> (vampire-prove '((:kind :occurrent-mereology))
                 '(:forall (?x ?y ?z) (:implies (:and (proper-occurrent-part-of ?x ?y) (proper-occurrent-part-of ?y ?z))
                                          (proper-occurrent-part-of ?x ?z))))
:proved

>> (get-vampire-proof-support)

(:definition-of-proper-occurrent-part-of :occurrent-part-of-is-antisymmetric :occurrent-part-of-transitive)

>> (vampire-prove '(:definition-of-proper-occurrent-part-of :occurrent-part-of-transitive) 
                      '(:forall (?x ?y ?z) (:implies (:and (proper-occurrent-part-of ?x ?y) (proper-occurrent-part-of ?y ?z))
                                               (proper-occurrent-part-of ?x ?z))))

:failed

>> (z3-find-model '(:definition-of-proper-occurrent-part-of :occurrent-part-of-transitive 
                        (:not (:forall (?x ?y ?z) (:implies (:and (proper-occurrent-part-of ?x ?y) (proper-occurrent-part-of ?y ?z))
                                               (proper-occurrent-part-of ?x ?z))))))

#<z3-model domain size 3, 2 predicates, 15 tuples>

>> (pprint-model *)
(proper-occurrent-part-of c2 c3)
(proper-occurrent-part-of c2 c1)
(proper-occurrent-part-of c3 c2)
(proper-occurrent-part-of c3 c1)
(proper-occurrent-part-of c1 c2)
(proper-occurrent-part-of c1 c3)
(occurrent-part-of c2 c2)
(occurrent-part-of c2 c3)
(occurrent-part-of c2 c1)
(occurrent-part-of c3 c2)
(occurrent-part-of c3 c3)
(occurrent-part-of c3 c1)
(occurrent-part-of c1 c2)
(occurrent-part-of c1 c3)
(occurrent-part-of c1 c1)

[alanruttenberg]

Here's a smaller model (courtesy of mace4)

(occurrent-part-of c1 c1)
(occurrent-part-of c1 c2)
(occurrent-part-of c2 c1)
(occurrent-part-of c2 c2)
(proper-occurrent-part-of c1 c2)
(proper-occurrent-part-of c2 c1)

[wceusters]

I realize that my earlier attempt to prove manually was wrong (printed here again since I accidently deleted the comment): Proper-occurrent-part-of a b input (1) Occurrent-part-of a b okr-1/(1) (2) Not = a b okr-1/(1) (3) Proper-occurrent-part-of b c input (4) Occurrent-part-of b c okr-1/(4) (5) Not = b c okr-1/(4) (6) Occurrent-part-of a c kad-1/(2)/(5) (7) Not = a c (3)/(6) (8) Proper-occurrent-part-of a c okr-1/(8)/(7) !

(8) does not follow from (3) and (6) as under these, it would also be possible that a = c.

So assume a = c

assume = a c (8b) proper-occurrent-part-of c b (1)/(8b) (9) occurrent-part-of c b okr-1/(9) (10) = c b xlu-1/(10)/(5) (11) contradiction (11)/(6)

Thus assumption (8b) is wrong, hence not = a c where we are back above and thus proper-occurrent-part-of a c.

[alanruttenberg]

fixed now