implication class restrictions of the form A -> B

classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

implication class restrictions of the form A -> B

Jan Scheffczyk
Hi all,

I want to implement class restrictions of the form A -> B, where A and B
are class restrictions themselves.
An example would be the following:
Assume we have classes T, T1, T2 and a property t_prop with domain T and
range T1 union T2.
Then I would like to have the following class restriction for class T

        t_prop min 2     ->    exists t_prop T2


So my idea was to first define an extra class T0 that contains by
definition all individuals that satisfy the antecedent of the above
implication.
Then the consequent of the above implication should be an additional
restriction on class T0.
T0 should be a subclass of T and is defined by the necessary and
sufficient condition:

        t_prop min 2

and the following additional restriction:

        exists t_prop T2

I thought that a reasoner like Racer could then infer instances of the
class T0.
For example, if we have instances

        t : T
        t1 : T1
        t2 : T2

and the following properties for the instance t

        t t_prop T1
        t t_prop T2

I would expect that Racer could infer that t is also a member of class
T0 since it satisfies the defining condition for T0.
However, Racer cannot infer that t : T0.

So what did I miss?

Any help in this matter would be greatly appreciated.

Many Thanks,
Jan
-------------------------------------------------------------------------
To unsubscribe go to http://protege.stanford.edu/community/subscribe.html

Reply | Threaded
Open this post in threaded view
|

[protege-owl] Re: implication class restrictions of the form A -> B

Matthew Horridge
Hi Jan,

Unfortunately, the current version of protege-owl does not support  
these kinds of axioms (know as general inclusion axioms - GCIs).  You  
can get around this by creating a named class and using it as a  
holder.  For example, if you create the class Axiom1 you can then add  
the left hand side of you GCI as an equivalent class to Axiom1 - i.e.  
a Necessary&Sufficient condition, and then add the right hand side of  
you GCI as a necessary conditions. So (using your notation) ....

Axiom <->  t_prop min 2
Axiom -> exists t_prop T2

Cheers,

Matthew





On 17 May 2006, at 16:10, Jan Scheffczyk wrote:

> Hi all,
>
> I want to implement class restrictions of the form A -> B, where A  
> and B are class restrictions themselves.
> An example would be the following:
> Assume we have classes T, T1, T2 and a property t_prop with domain  
> T and range T1 union T2.
> Then I would like to have the following class restriction for class T
>
> t_prop min 2     ->    exists t_prop T2
>
>
> So my idea was to first define an extra class T0 that contains by  
> definition all individuals that satisfy the antecedent of the above  
> implication.
> Then the consequent of the above implication should be an  
> additional restriction on class T0.
> T0 should be a subclass of T and is defined by the necessary and  
> sufficient condition:
>
> t_prop min 2
>
> and the following additional restriction:
>
> exists t_prop T2
>
> I thought that a reasoner like Racer could then infer instances of  
> the class T0.
> For example, if we have instances
>
> t : T
> t1 : T1
> t2 : T2
>
> and the following properties for the instance t
>
> t t_prop T1
> t t_prop T2
>
> I would expect that Racer could infer that t is also a member of  
> class T0 since it satisfies the defining condition for T0.
> However, Racer cannot infer that t : T0.
>
> So what did I miss?
>
> Any help in this matter would be greatly appreciated.
>
> Many Thanks,
> Jan
> ----------------------------------------------------------------------
> ---
> To unsubscribe go to http://protege.stanford.edu/community/ 
> subscribe.html
>

-------------------------------------------------------------------------
To unsubscribe go to http://protege.stanford.edu/community/subscribe.html

Reply | Threaded
Open this post in threaded view
|

[protege-owl] Re: implication class restrictions of the form A -> B

Jan Scheffczyk
Hi Matthew,

I did exactly as you said and tried both Racer and FaCT++:

> Axiom <->  t_prop min 2

Classifying the ontology results in making Axiom a subclass of T, which
I can perfectly understand.

Then I created instances, in order to test whether the reasoner can
infer that some instances are members of class Axiom:

        instance t of class T
        instance t1 of class T1
        instance t2 of class T2

and I connected

        t to t2 via t_prop
        t to t1 via t_prop

So, instance t satisfies the necessary & sufficient condition of class
Axiom, whereas instances t1 and t2 do not.
I would expect that a reasoner could infer that instance t is a member
of Axiom.

Running type inference for instance t shows, however, class T only (and
not Axiom), which I think is not correct given above definitions.
Running type inference for all instances does not show instance t as an
inferred instance of class Axiom either.

Do you understand this behavior?

Attached you find the OWL file, maybe I just did something wrong.

Many thanks for your help.

Cheers,
Jan

<?xml version="1.0"?>
<rdf:RDF
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
    xmlns:owl="http://www.w3.org/2002/07/owl#"
    xmlns="http://www.icsi.berkeley.edu/~jan/ocl2owl.owl#"
  xml:base="http://www.icsi.berkeley.edu/~jan/ocl2owl.owl">
  <owl:Ontology rdf:about=""/>
  <owl:Class rdf:ID="T"/>
  <owl:Class rdf:ID="T1"/>
  <owl:Class rdf:ID="Axiom">
    <owl:equivalentClass>
      <owl:Restriction>
        <owl:onProperty>
          <owl:ObjectProperty rdf:ID="t_prop"/>
        </owl:onProperty>
        <owl:minCardinality rdf:datatype="http://www.w3.org/2001/XMLSchema#int"
        >2</owl:minCardinality>
      </owl:Restriction>
    </owl:equivalentClass>
  </owl:Class>
  <owl:Class rdf:ID="T2"/>
  <owl:ObjectProperty rdf:about="#t_prop">
    <rdfs:domain rdf:resource="#T"/>
    <rdfs:range>
      <owl:Class>
        <owl:unionOf rdf:parseType="Collection">
          <owl:Class rdf:about="#T1"/>
          <owl:Class rdf:about="#T2"/>
        </owl:unionOf>
      </owl:Class>
    </rdfs:range>
  </owl:ObjectProperty>
  <T rdf:ID="t">
    <t_prop>
      <T1 rdf:ID="t1"/>
    </t_prop>
    <t_prop>
      <T2 rdf:ID="t2"/>
    </t_prop>
  </T>
</rdf:RDF>

<!-- Created with Protege (with OWL Plugin 2.2, Build 311)  http://protege.stanford.edu -->
Reply | Threaded
Open this post in threaded view
|

[protege-owl] Re: implication class restrictions of the form A -> B

Hai Wang
Hi Jan,
You need to assert that t1 and t2 are two different instances. OWL  
does not use UMA (Unique name assumption) which means that two  
different names could refer to one same object.

You can do it by go to
OWL--> Edit OWL:allDifferent ..

Cheers
Hai

On 18 May 2006, at 15:59, Jan Scheffczyk wrote:

> Hi Matthew,
>
> I did exactly as you said and tried both Racer and FaCT++:
>
>> Axiom <->  t_prop min 2
>
> Classifying the ontology results in making Axiom a subclass of T,  
> which I can perfectly understand.
>
> Then I created instances, in order to test whether the reasoner can  
> infer that some instances are members of class Axiom:
>
> instance t of class T
> instance t1 of class T1
> instance t2 of class T2
>
> and I connected
>
> t to t2 via t_prop
> t to t1 via t_prop
>
> So, instance t satisfies the necessary & sufficient condition of  
> class Axiom, whereas instances t1 and t2 do not.
> I would expect that a reasoner could infer that instance t is a  
> member of Axiom.
>
> Running type inference for instance t shows, however, class T only  
> (and not Axiom), which I think is not correct given above definitions.
> Running type inference for all instances does not show instance t  
> as an inferred instance of class Axiom either.
>
> Do you understand this behavior?
>
> Attached you find the OWL file, maybe I just did something wrong.
>
> Many thanks for your help.
>
> Cheers,
> Jan
> <?xml version="1.0"?>
> <rdf:RDF
>     xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
>     xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
>     xmlns:owl="http://www.w3.org/2002/07/owl#"
>     xmlns="http://www.icsi.berkeley.edu/~jan/ocl2owl.owl#"
>   xml:base="http://www.icsi.berkeley.edu/~jan/ocl2owl.owl">
>   <owl:Ontology rdf:about=""/>
>   <owl:Class rdf:ID="T"/>
>   <owl:Class rdf:ID="T1"/>
>   <owl:Class rdf:ID="Axiom">
>     <owl:equivalentClass>
>       <owl:Restriction>
>         <owl:onProperty>
>           <owl:ObjectProperty rdf:ID="t_prop"/>
>         </owl:onProperty>
>         <owl:minCardinality rdf:datatype="http://www.w3.org/2001/ 
> XMLSchema#int"
>         >2</owl:minCardinality>
>       </owl:Restriction>
>     </owl:equivalentClass>
>   </owl:Class>
>   <owl:Class rdf:ID="T2"/>
>   <owl:ObjectProperty rdf:about="#t_prop">
>     <rdfs:domain rdf:resource="#T"/>
>     <rdfs:range>
>       <owl:Class>
>         <owl:unionOf rdf:parseType="Collection">
>           <owl:Class rdf:about="#T1"/>
>           <owl:Class rdf:about="#T2"/>
>         </owl:unionOf>
>       </owl:Class>
>     </rdfs:range>
>   </owl:ObjectProperty>
>   <T rdf:ID="t">
>     <t_prop>
>       <T1 rdf:ID="t1"/>
>     </t_prop>
>     <t_prop>
>       <T2 rdf:ID="t2"/>
>     </t_prop>
>   </T>
> </rdf:RDF>
>
> <!-- Created with Protege (with OWL Plugin 2.2, Build 311)  http://
> protege.stanford.edu -->

-------------------------------------------------------------------------
To unsubscribe go to http://protege.stanford.edu/community/subscribe.html

Reply | Threaded
Open this post in threaded view
|

[protege-owl] Re: implication class restrictions of the form A -> B

Jan Scheffczyk
Hi Hai,

thanks so much that was the solution :-)))

Cheers,
Jan

Hai Wang wrote:

> Hi Jan,
> You need to assert that t1 and t2 are two different instances. OWL does
> not use UMA (Unique name assumption) which means that two different
> names could refer to one same object.
>
> You can do it by go to
> OWL--> Edit OWL:allDifferent ..
>
> Cheers
> Hai
>
-------------------------------------------------------------------------
To unsubscribe go to http://protege.stanford.edu/community/subscribe.html