GoogleCodeExporter
commented
9 years ago We have many property chains, for example:
* has_part o part_of -> overlaps
How should these be translated to BFO2? Would the FOL group be able to help prove the correctness of the translation? I have some experience with the logical formalism but I personally find this quite hard.
It is work.
For example, in this particular case I would assume:
ObjectProperty: overlaps-continuant-at-some-times
Characteristics: Symmetric
yes
ObjectProperty: overlaps-continuant-at-all-times
SubPropertyOf: overlaps-continuant-at-some-times
There is a general pattern that rel at all times -> rel at some times. So yes.
ObjectProperty: overlaps-continuant-at-all-times-for-which-partner-exists
SubPropertyOf: overlaps-continuant-at-some-times
Yes
Existing relations would need to be added, creating a subproperty lattice.
E.g.
AddAxiom: part-of-continuant-at-some-times SubPropertyOf overlaps-continuant-at-some-times
AddAxiom: part-of-continuant-at-all-times SubPropertyOf overlaps-continuant-at-all-times
AddAxiom: part-of-continuant-at-all-times-for-which-part-exists SubPropertyOf overlaps-continuant-at-all-times-for-which-partner-exists
AddAxiom: has-continuant-part-at-some-times SubPropertyOf overlaps-continuant-at-some-times
AddAxiom: has-continuant-part-at-all-times SubPropertyOf overlaps-continuant-at-all-times
AddAxiom: has-continuant-part-at-all-times-for-which-whole-exists SubPropertyOf overlaps-continuant-at-all-times-for-which-partner-exists
Withough checking details, generally yes. In the current BFO build some amount
of this is done automatically, some manually, though in shorthand so it is
quicker.
Then for the property chains themselves, perhaps:
* has-continuant-part-at-some-times o part-of-continuant-at-all-times -> overlaps-continuant-at-some-times
* has-continuant-part-at-all-times o part-of-continuant-at-all-times -> overlaps-continuant-at-all-times
* has-continuant-part-at-all-times-for-which-whole-exists o part-of-continuant-at-all-times -> overlaps-continuant-at-all-times-for-which-partner-exists
I just made this list quickly based on rough intuition. I don't have strong confidence that they are correct, and I'm certain they're not complete.
In a similar vein, I'm not checking them carefully. But the intuition is
correct.
Is there a tool I could use to generate these axioms for any property chain (preferably with proofs that they are valid and that they are complete w.r.t what is possible in OWL)?
You are the best person to know this :)
Currently the lisp code does some of the generation, but doesn't do the proofs.
I would hope that the proofs arise either from the FOL groups, or from
consistency checking (of the FOL expression) for well chosen examples.
Is there any way we can know ahead of time if we are likely to start running into either OWL2 structural restrictions on axioms, or reasoner performance errors?
You can either try to grok the global restrictions and keep them in mind as you
write (hard - I can't) or you can check when it is reasoned. In practive the
violations I've found are by the latter method. I note them in the lisp spec,
marking them with ':cant "reason"' so they can be reviewed at a later time for
documentation purposes or to see if we can get the desired entailments without
hitting the restrictions. Below is a current grep for :cant in
trunk/src/ontology/owl-group/specification
binary-relation-axioms.lisp: (occurrent -> self :cant "Non-simple property or
its inverse appears in the Self restriction")
binary-relation-axioms.lisp: (< (occurrent -> self :cant "Non-simple property
or its inverse appears in the Self restriction"))
binary-relation-axioms.lisp: (0d-t-region -> self :id 145 :cant "Non-simple
property or its inverse appears in the Self restriction")
binary-relation-axioms.lisp: (o occupies st-projects-onto-t :id 168 :cant
"conflicts with the self properties. Recast the self properties using new
relations to get around this")
temporal-relation-axioms.lisp: (s (o has-participant_st inheres-in_at :id 561
:cant "There is a cyclic dependency involving property has-participant_st"))
temporal-relation-axioms.lisp: (a (o bearer-of_at participates-in_at :id 562
:cant "There is a cyclic dependency involving property has-participant_at"))
temporal-relation-axioms.lisp: (< (a (o has-g-dep_at participates-in_at :id
571 :cant "There is a cyclic dependency involving property
has-participant_at")))
temporal-relation-axioms.lisp: (< (s (o has-g-dep_st participates-in_at :id
572 :cant "The given property hierarchy is not regular. There is a cyclic
dependency involving property 'participates in at some time'")))
Original comment by alanruttenberg@gmail.com on 12 Mar 2013 at 5:53
Original issue reported on code.google.com by
cmung...@gmail.comon 9 Mar 2013 at 10:19