towards generic parthood

[Alan Ruttenberg]

I believe this GCI expresses generic-part-of-at-all-times, between a nucleus and a cell, with the statements, however, made of the histories.

(temporal-part-of some history-of some nucleus)

SubClassOf:

(overlaps some (temporal-part-of some history of some cell))

That is:

Recall that history of nucleus is 1:1 with nucleus and that

if, for some period of time, a temporal part of a history of x is a temporal part of a history of y then 

x is part of y during that time.

Now:

Pick any temporal part of some history of some nucleus. (the lhs of the GCI)

there will exist some temporal part of some history of some cell such that

the temporal parts overlap (the rhs)

During that overlap, the nucleus will be part of that cell.

Since this is true of any temporal part of any history of a nucleus, it will be true always. But note there is no constraint that the cells are the same (since different cell histories can be chosen to satisfy each challenge temporal part of the history of the nucleus.

Anyone have a contradiction?

-Alan

[Alan Ruttenberg]

It's transitive too.

Example attached.

[Chris Mungall]

Did you mean to declare overlaps to be transitive?

--
You received this message because you are subscribed to the Google Groups "bfo-owl-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email to bfo-owl-deve...@googlegroups.com.
To post to this group, send email to bfo-ow...@googlegroups.com.
Visit this group at http://groups.google.com/group/bfo-owl-devel?hl=en-US.
For more options, visit https://groups.google.com/groups/opt_out.
 
 
<permanent-generic-part-of.owl>

[Alan Ruttenberg]

No, error. 

Kills transitive, but I will work on it.

Thanks for the catch.

-Alan

[Chris Mungall]

Change it to has-occurrent-part and the example works (attached).

Can we get an OWL reasoner to derive the following?

P part-of-at-all-times W

implies

temporal-part-of some (history-of some P) SubClassOf 'has occurrent part' some (temporal-part-of some (history-of some W))

implies

P part-of-at-some-times W

[Alan Ruttenberg]

On Tue, Apr 30, 2013 at 10:43 AM, Chris Mungall <cjmu...@lbl.gov> wrote:

Change it to has-occurrent-part and the example works (attached).

Ah, right. If it overlaps, then you can take the overlapping part and shrink it until it is just part. :)

(has-part in my example is has-occurrent-part, double verified by making the substitution in my file)

Can we get an OWL reasoner to derive the following?

i.e.

nucleus part-of-at-all-times some cell

=>

nucleus permanent-generic-part-of cell

I'll look. 

We should prove the permanent-generic-parthood using snark/prover9.

--Alan

P part-of-at-all-times W

implies

temporal-part-of some (history-of some P) SubClassOf 'has occurrent part' some (temporal-part-of some (history-of some W))

implies

P part-of-at-some-times W

[Alan Ruttenberg]

I checked in the example 

https://bfo.googlecode.com/svn/trunk/src/ontology/owl-group/examples/permanent-generic-part-of.owl