previous next top contents index

OWL Web Ontology Language
Test Cases
C.5.1. Arithmetic in OWL


Contents


C.5.1. Arithmetic in OWL

Tests that show the relationship between OWL and simple arithmetic.

FullPositive Entailment Test:002
Description: (informative) <extra-credit/Manifest002#test>
This test shows a relationship between integer multiplication and OWL Full.
Required datatype support: xsd:int,
N3 format is informative.
FullPremises: <extra-credit/premises002>
<rdf:RDF
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:owl="http://www.w3.org/2002/07/owl#"
    xmlns:rdfs= "http://www.w3.org/2000/01/rdf-schema#"
    xml:base="http://www.w3.org/2002/03owlt/extra-credit/premises002" >

   <owl:FunctionalProperty rdf:ID="p-N-to-1" >
     <owl:inverseOf>
       <owl:ObjectProperty rdf:ID="invP-1-to-N" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N" />
     <rdfs:range rdf:resource="#only-d" />
   </owl:FunctionalProperty>
   <owl:FunctionalProperty rdf:ID="q-M-to-1" >
     <owl:inverseOf>
        <owl:ObjectProperty rdf:ID="invQ-1-to-M" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N-times-M" />
     <rdfs:range rdf:resource="#cardinality-N" />
   </owl:FunctionalProperty>
   <owl:FunctionalProperty rdf:ID="r-N-times-M-to-1">
     <owl:inverseOf>
        <owl:ObjectProperty  rdf:ID="invR-1-to-N-times-M" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N-times-M" />
     <rdfs:range rdf:resource="#only-d" />
   </owl:FunctionalProperty>
   
    <owl:Class rdf:ID="only-d">
      <owl:oneOf rdf:parseType="Collection">
         <rdf:Description rdf:ID="d"/>
      </owl:oneOf>
      <owl:equivalentClass>
        <owl:Restriction>
          <owl:onProperty rdf:resource="#invP-1-to-N"/>
          <owl:cardinality rdf:resource="#N"/>
        </owl:Restriction>
      </owl:equivalentClass>
      <owl:equivalentClass>
         <owl:Restriction>
           <owl:onProperty rdf:resource="#invR-N-times-M-to-1"/>
           <owl:cardinality rdf:resource="#N-times-M"/>
         </owl:Restriction>
      </owl:equivalentClass>
    </owl:Class>
    <owl:Class rdf:ID="cardinality-N">
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#p-N-to-1"/>
             <owl:someValuesFrom rdf:resource="#only-d"/>
           </owl:Restriction>
       </owl:equivalentClass>
       <owl:equivalentClass>
           <owl:Restriction>
              <owl:onProperty rdf:resource="#invQ-1-to-M"/>
              <owl:cardinality rdf:resource="#M"/>
           </owl:Restriction>
       </owl:equivalentClass>
    </owl:Class>
    <owl:Class rdf:ID="cardinality-N-times-M">
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#q-M-to-1"/>
             <owl:someValuesFrom rdf:resource="#cardinality-N"/>
           </owl:Restriction>
       </owl:equivalentClass>
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#r-N-times-M-to-1"/>
             <owl:someValuesFrom rdf:resource="#only-d"/>
           </owl:Restriction>
       </owl:equivalentClass>
    </owl:Class>

    <rdf:Description rdf:about="#N">
      <owl:sameIndividualAs 
          rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">15</owl:sameIndividualAs>
     </rdf:Description>
    <rdf:Description rdf:about="#M">
      <owl:sameIndividualAs 
          rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">23</owl:sameIndividualAs>
     </rdf:Description>

</rdf:RDF>
first:p-N-to-1 rdf:type owl:FunctionalProperty .
first:invP-1-to-N rdf:type owl:ObjectProperty .
first:p-N-to-1 owl:inverseOf first:invP-1-to-N .
first:p-N-to-1 rdfs:domain first:cardinality-N .
first:p-N-to-1 rdfs:range first:only-d .
first:q-M-to-1 rdf:type owl:FunctionalProperty .
first:invQ-1-to-M rdf:type owl:ObjectProperty .
first:q-M-to-1 owl:inverseOf first:invQ-1-to-M .
first:q-M-to-1 rdfs:domain first:cardinality-N-times-M .
first:q-M-to-1 rdfs:range first:cardinality-N .
first:r-N-times-M-to-1 rdf:type owl:FunctionalProperty .
first:invR-1-to-N-times-M rdf:type owl:ObjectProperty .
first:r-N-times-M-to-1 owl:inverseOf first:invR-1-to-N-times-M .
first:r-N-times-M-to-1 rdfs:domain first:cardinality-N-times-M .
first:r-N-times-M-to-1 rdfs:range first:only-d .
first:only-d rdf:type owl:Class .
_:a rdf:first first:d .
_:a rdf:rest rdf:nil .
_:a rdf:type rdf:List .
first:only-d owl:oneOf _:a .
_:c rdf:type owl:Restriction .
_:c owl:onProperty first:invP-1-to-N .
_:c owl:cardinality first:N .
first:only-d owl:equivalentClass _:c .
_:e rdf:type owl:Restriction .
_:e owl:onProperty first:invR-N-times-M-to-1 .
_:e owl:cardinality first:N-times-M .
first:only-d owl:equivalentClass _:e .
first:cardinality-N rdf:type owl:Class .
_:g rdf:type owl:Restriction .
_:g owl:onProperty first:p-N-to-1 .
_:g owl:someValuesFrom first:only-d .
first:cardinality-N owl:equivalentClass _:g .
_:i rdf:type owl:Restriction .
_:i owl:onProperty first:invQ-1-to-M .
_:i owl:cardinality first:M .
first:cardinality-N owl:equivalentClass _:i .
first:cardinality-N-times-M rdf:type owl:Class .
_:k rdf:type owl:Restriction .
_:k owl:onProperty first:q-M-to-1 .
_:k owl:someValuesFrom first:cardinality-N .
first:cardinality-N-times-M owl:equivalentClass _:k .
_:m rdf:type owl:Restriction .
_:m owl:onProperty first:r-N-times-M-to-1 .
_:m owl:someValuesFrom first:only-d .
first:cardinality-N-times-M owl:equivalentClass _:m .
first:N owl:sameIndividualAs "15"^^xsd:int  .
first:M owl:sameIndividualAs "23"^^xsd:int  .
FullConclusions: <extra-credit/conclusions002>
<rdf:RDF
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:owl="http://www.w3.org/2002/07/owl#"
    xml:base="http://www.w3.org/2002/03owlt/extra-credit/conclusions002" >

    <rdf:Description rdf:about="premises002#N-times-M">
      <owl:sameIndividualAs 
          rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">345</owl:sameIndividualAs>
     </rdf:Description>

</rdf:RDF>
first:N-times-M owl:sameIndividualAs "345"^^xsd:int  .

FullPositive Entailment Test:003
Description: (informative) <extra-credit/Manifest003#test>
Prime factorization can be expressed in OWL Full.
Required datatype support: xsd:int,
N3 format is informative.
FullPremises: <extra-credit/premises003>
<rdf:RDF
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:owl="http://www.w3.org/2002/07/owl#"
    xmlns:rdfs= "http://www.w3.org/2000/01/rdf-schema#"
    xml:base="http://www.w3.org/2002/03owlt/extra-credit/premises003" >

   <owl:FunctionalProperty rdf:ID="p-N-to-1" >
     <owl:inverseOf>
       <owl:ObjectProperty rdf:ID="invP-1-to-N" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N" />
     <rdfs:range rdf:resource="#only-d" />
   </owl:FunctionalProperty>
   <owl:FunctionalProperty rdf:ID="q-M-to-1" >
     <owl:inverseOf>
        <owl:ObjectProperty rdf:ID="invQ-1-to-M" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N-times-M" />
     <rdfs:range rdf:resource="#cardinality-N" />
   </owl:FunctionalProperty>
   <owl:FunctionalProperty rdf:ID="r-N-times-M-to-1">
     <owl:inverseOf>
        <owl:ObjectProperty  rdf:ID="invR-1-to-N-times-M" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N-times-M" />
     <rdfs:range rdf:resource="#only-d" />
   </owl:FunctionalProperty>
   
    <owl:Class rdf:ID="only-d">
      <owl:oneOf rdf:parseType="Collection">
         <rdf:Description rdf:ID="d"/>
      </owl:oneOf>
      <owl:equivalentClass>
        <owl:Restriction>
          <owl:onProperty rdf:resource="#invP-1-to-N"/>
          <owl:cardinality rdf:resource="#N"/>
        </owl:Restriction>
      </owl:equivalentClass>
      <owl:equivalentClass>
         <owl:Restriction>
           <owl:onProperty rdf:resource="#invR-N-times-M-to-1"/>
           <owl:cardinality rdf:resource="#N-times-M"/>
         </owl:Restriction>
      </owl:equivalentClass>
    </owl:Class>
    <owl:Class rdf:ID="cardinality-N">
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#p-N-to-1"/>
             <owl:someValuesFrom rdf:resource="#only-d"/>
           </owl:Restriction>
       </owl:equivalentClass>
       <owl:equivalentClass>
           <owl:Restriction>
              <owl:onProperty rdf:resource="#invQ-1-to-M"/>
              <owl:cardinality rdf:resource="#M"/>
           </owl:Restriction>
       </owl:equivalentClass>
    </owl:Class>
    <owl:Class rdf:ID="cardinality-N-times-M">
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#q-M-to-1"/>
             <owl:someValuesFrom rdf:resource="#cardinality-N"/>
           </owl:Restriction>
       </owl:equivalentClass>
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#r-N-times-M-to-1"/>
             <owl:someValuesFrom rdf:resource="#only-d"/>
           </owl:Restriction>
       </owl:equivalentClass>
    </owl:Class>

    <rdf:Description rdf:about="#N-times-M">
      <owl:sameIndividualAs 
          rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">77</owl:sameIndividualAs>
     </rdf:Description>

</rdf:RDF>
first:p-N-to-1 rdf:type owl:FunctionalProperty .
first:invP-1-to-N rdf:type owl:ObjectProperty .
first:p-N-to-1 owl:inverseOf first:invP-1-to-N .
first:p-N-to-1 rdfs:domain first:cardinality-N .
first:p-N-to-1 rdfs:range first:only-d .
first:q-M-to-1 rdf:type owl:FunctionalProperty .
first:invQ-1-to-M rdf:type owl:ObjectProperty .
first:q-M-to-1 owl:inverseOf first:invQ-1-to-M .
first:q-M-to-1 rdfs:domain first:cardinality-N-times-M .
first:q-M-to-1 rdfs:range first:cardinality-N .
first:r-N-times-M-to-1 rdf:type owl:FunctionalProperty .
first:invR-1-to-N-times-M rdf:type owl:ObjectProperty .
first:r-N-times-M-to-1 owl:inverseOf first:invR-1-to-N-times-M .
first:r-N-times-M-to-1 rdfs:domain first:cardinality-N-times-M .
first:r-N-times-M-to-1 rdfs:range first:only-d .
first:only-d rdf:type owl:Class .
_:a rdf:first first:d .
_:a rdf:rest rdf:nil .
_:a rdf:type rdf:List .
first:only-d owl:oneOf _:a .
_:c rdf:type owl:Restriction .
_:c owl:onProperty first:invP-1-to-N .
_:c owl:cardinality first:N .
first:only-d owl:equivalentClass _:c .
_:e rdf:type owl:Restriction .
_:e owl:onProperty first:invR-N-times-M-to-1 .
_:e owl:cardinality first:N-times-M .
first:only-d owl:equivalentClass _:e .
first:cardinality-N rdf:type owl:Class .
_:g rdf:type owl:Restriction .
_:g owl:onProperty first:p-N-to-1 .
_:g owl:someValuesFrom first:only-d .
first:cardinality-N owl:equivalentClass _:g .
_:i rdf:type owl:Restriction .
_:i owl:onProperty first:invQ-1-to-M .
_:i owl:cardinality first:M .
first:cardinality-N owl:equivalentClass _:i .
first:cardinality-N-times-M rdf:type owl:Class .
_:k rdf:type owl:Restriction .
_:k owl:onProperty first:q-M-to-1 .
_:k owl:someValuesFrom first:cardinality-N .
first:cardinality-N-times-M owl:equivalentClass _:k .
_:m rdf:type owl:Restriction .
_:m owl:onProperty first:r-N-times-M-to-1 .
_:m owl:someValuesFrom first:only-d .
first:cardinality-N-times-M owl:equivalentClass _:m .
first:N-times-M owl:sameIndividualAs "77"^^xsd:int  .
FullConclusions: <extra-credit/conclusions003>
<rdf:RDF
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:owl="http://www.w3.org/2002/07/owl#"
    xml:base="http://www.w3.org/2002/03owlt/extra-credit/conclusions003" >
    
    <owl:Class>
         <owl:oneOf rdf:parseType="Collection">
            <rdf:Description rdf:about="premises003#N"/>
            <rdf:Description rdf:about="premises003#M"/>
         </owl:oneOf>
         <owl:oneOf rdf:parseType="Collection">
            <rdf:Description>
              <owl:sameIndividualAs rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">7</owl:sameIndividualAs>
            </rdf:Description>
            <rdf:Description>
              <owl:sameIndividualAs rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">11</owl:sameIndividualAs>
            </rdf:Description>
         </owl:oneOf>
    </owl:Class>
</rdf:RDF>
_:a rdf:type owl:Class .
_:c rdf:first first:M .
_:c rdf:rest rdf:nil .
_:c rdf:type rdf:List .
_:e rdf:first first:N .
_:e rdf:rest _:c .
_:e rdf:type rdf:List .
_:a owl:oneOf _:e .
_:g owl:sameIndividualAs "7"^^xsd:int  .
_:i owl:sameIndividualAs "11"^^xsd:int  .
_:k rdf:first _:i .
_:k rdf:rest rdf:nil .
_:k rdf:type rdf:List .
_:m rdf:first _:g .
_:m rdf:rest _:k .
_:m rdf:type rdf:List .
_:a owl:oneOf _:m .

FullPositive Entailment Test:004
Description: (informative) <extra-credit/Manifest004#test>
A more difficult prime factorization example.
Required datatype support: xsd:int,
N3 format is informative.
FullPremises: <extra-credit/premises004>
<rdf:RDF
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:owl="http://www.w3.org/2002/07/owl#"
    xml:base="http://www.w3.org/2002/03owlt/extra-credit/premises004" 
    xmlns:rdfs= "http://www.w3.org/2000/01/rdf-schema#">

   <owl:FunctionalProperty rdf:ID="p-N-to-1" >
     <owl:inverseOf>
       <owl:ObjectProperty rdf:ID="invP-1-to-N" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N" />
     <rdfs:range rdf:resource="#only-d" />
   </owl:FunctionalProperty>
   <owl:FunctionalProperty rdf:ID="q-M-to-1" >
     <owl:inverseOf>
        <owl:ObjectProperty rdf:ID="invQ-1-to-M" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N-times-M" />
     <rdfs:range rdf:resource="#cardinality-N" />
   </owl:FunctionalProperty>
   <owl:FunctionalProperty rdf:ID="r-N-times-M-to-1">
     <owl:inverseOf>
        <owl:ObjectProperty  rdf:ID="invR-1-to-N-times-M" />
     </owl:inverseOf>
     <rdfs:domain rdf:resource="#cardinality-N-times-M" />
     <rdfs:range rdf:resource="#only-d" />
   </owl:FunctionalProperty>
   
    <owl:Class rdf:ID="only-d">
      <owl:oneOf rdf:parseType="Collection">
         <rdf:Description rdf:ID="d"/>
      </owl:oneOf>
      <owl:equivalentClass>
        <owl:Restriction>
          <owl:onProperty rdf:resource="#invP-1-to-N"/>
          <owl:cardinality rdf:resource="#N"/>
        </owl:Restriction>
      </owl:equivalentClass>
      <owl:equivalentClass>
         <owl:Restriction>
           <owl:onProperty rdf:resource="#invR-N-times-M-to-1"/>
           <owl:cardinality rdf:resource="#N-times-M"/>
         </owl:Restriction>
      </owl:equivalentClass>
    </owl:Class>
    <owl:Class rdf:ID="cardinality-N">
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#p-N-to-1"/>
             <owl:someValuesFrom rdf:resource="#only-d"/>
           </owl:Restriction>
       </owl:equivalentClass>
       <owl:equivalentClass>
           <owl:Restriction>
              <owl:onProperty rdf:resource="#invQ-1-to-M"/>
              <owl:cardinality rdf:resource="#M"/>
           </owl:Restriction>
       </owl:equivalentClass>
    </owl:Class>
    <owl:Class rdf:ID="cardinality-N-times-M">
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#q-M-to-1"/>
             <owl:someValuesFrom rdf:resource="#cardinality-N"/>
           </owl:Restriction>
       </owl:equivalentClass>
       <owl:equivalentClass>
           <owl:Restriction>
             <owl:onProperty rdf:resource="#r-N-times-M-to-1"/>
             <owl:someValuesFrom rdf:resource="#only-d"/>
           </owl:Restriction>
       </owl:equivalentClass>
    </owl:Class>
   
    <rdf:Description rdf:about="#N-times-M">
      <owl:sameIndividualAs 
          rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">929136997</owl:sameIndividualAs>
     </rdf:Description>

</rdf:RDF>
first:p-N-to-1 rdf:type owl:FunctionalProperty .
first:invP-1-to-N rdf:type owl:ObjectProperty .
first:p-N-to-1 owl:inverseOf first:invP-1-to-N .
first:p-N-to-1 rdfs:domain first:cardinality-N .
first:p-N-to-1 rdfs:range first:only-d .
first:q-M-to-1 rdf:type owl:FunctionalProperty .
first:invQ-1-to-M rdf:type owl:ObjectProperty .
first:q-M-to-1 owl:inverseOf first:invQ-1-to-M .
first:q-M-to-1 rdfs:domain first:cardinality-N-times-M .
first:q-M-to-1 rdfs:range first:cardinality-N .
first:r-N-times-M-to-1 rdf:type owl:FunctionalProperty .
first:invR-1-to-N-times-M rdf:type owl:ObjectProperty .
first:r-N-times-M-to-1 owl:inverseOf first:invR-1-to-N-times-M .
first:r-N-times-M-to-1 rdfs:domain first:cardinality-N-times-M .
first:r-N-times-M-to-1 rdfs:range first:only-d .
first:only-d rdf:type owl:Class .
_:a rdf:first first:d .
_:a rdf:rest rdf:nil .
_:a rdf:type rdf:List .
first:only-d owl:oneOf _:a .
_:c rdf:type owl:Restriction .
_:c owl:onProperty first:invP-1-to-N .
_:c owl:cardinality first:N .
first:only-d owl:equivalentClass _:c .
_:e rdf:type owl:Restriction .
_:e owl:onProperty first:invR-N-times-M-to-1 .
_:e owl:cardinality first:N-times-M .
first:only-d owl:equivalentClass _:e .
first:cardinality-N rdf:type owl:Class .
_:g rdf:type owl:Restriction .
_:g owl:onProperty first:p-N-to-1 .
_:g owl:someValuesFrom first:only-d .
first:cardinality-N owl:equivalentClass _:g .
_:i rdf:type owl:Restriction .
_:i owl:onProperty first:invQ-1-to-M .
_:i owl:cardinality first:M .
first:cardinality-N owl:equivalentClass _:i .
first:cardinality-N-times-M rdf:type owl:Class .
_:k rdf:type owl:Restriction .
_:k owl:onProperty first:q-M-to-1 .
_:k owl:someValuesFrom first:cardinality-N .
first:cardinality-N-times-M owl:equivalentClass _:k .
_:m rdf:type owl:Restriction .
_:m owl:onProperty first:r-N-times-M-to-1 .
_:m owl:someValuesFrom first:only-d .
first:cardinality-N-times-M owl:equivalentClass _:m .
first:N-times-M owl:sameIndividualAs "929136997"^^xsd:int  .
FullConclusions: <extra-credit/conclusions004>
<rdf:RDF
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:owl="http://www.w3.org/2002/07/owl#"
    xml:base="http://www.w3.org/2002/03owlt/extra-credit/conclusions004" >
    
    <owl:Class>
         <owl:oneOf rdf:parseType="Collection">
            <rdf:Description rdf:about="premises004#N"/>
            <rdf:Description rdf:about="premises004#M"/>
         </owl:oneOf>
         <owl:oneOf rdf:parseType="Collection">
            <rdf:Description>
              <owl:sameIndividualAs rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">83563</owl:sameIndividualAs>
            </rdf:Description>
            <rdf:Description>
              <owl:sameIndividualAs rdf:datatype=
"http://www.w3.org/2001/XMLSchema#int">11119</owl:sameIndividualAs>
            </rdf:Description>
         </owl:oneOf>
    </owl:Class>
</rdf:RDF>
_:a rdf:type owl:Class .
_:c rdf:first first:M .
_:c rdf:rest rdf:nil .
_:c rdf:type rdf:List .
_:e rdf:first first:N .
_:e rdf:rest _:c .
_:e rdf:type rdf:List .
_:a owl:oneOf _:e .
_:g owl:sameIndividualAs "83563"^^xsd:int  .
_:i owl:sameIndividualAs "11119"^^xsd:int  .
_:k rdf:first _:i .
_:k rdf:rest rdf:nil .
_:k rdf:type rdf:List .
_:m rdf:first _:g .
_:m rdf:rest _:k .
_:m rdf:type rdf:List .
_:a owl:oneOf _:m .


previous next top contents index