BFO-ontology/BFO

Provide help for translating property chains to BFO2

Opened this issue · 1 comments

zhengj2007 commented

From cmung...@gmail.com on March 09, 2013 17:19:49

We have many property chains, for example:

  • has_part o part_of -> overlaps

(note we need SWRL to properly define overlaps, but this property chain is good for some purposes).

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.

For example, in this particular case I would assume:

ObjectProperty: overlaps-continuant-at-some-times
Characteristics: Symmetric

ObjectProperty: overlaps-continuant-at-all-times
SubPropertyOf: overlaps-continuant-at-some-times

ObjectProperty: overlaps-continuant-at-all-times-for-which-partner-exists
SubPropertyOf: overlaps-continuant-at-some-times

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

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.

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)?

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?

Original issue: http://code.google.com/p/bfo/issues/detail?id=157

zhengj2007 commented

From alanruttenberg@gmail.com on March 12, 2013 10:53:49

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'")))