SWAD-Europe: WP5.3 XML Test Cases

Project name:
Semantic Web Advanced Development for Europe (SWAD-Europe)
Project Number:
IST-2001-34732
Workpackage name:
SWAD-Europe: Integration with XML Technology
Workpackage description:
http://www.w3.org/2001/sw/Europe/plan/workpackages/live/esw-wp-5.html
Deliverable title:
5.3 RDF/XML Test cases for RDF Logic, Web Ontology and Maths content
URI:
Authors:
Stephen Buswell, Stilo Technology
Abstract:
Examples of Multi-Namespace XML Content
Status:

Comments on this document should be sent to Stephen Buswell,

Contents

Introduction

This paper is part of SWAD-E Workpackage 5.3, concerned with multiple-namespace XML content. It takes as an example data from the OpenMath and MONET projects.

OpenMath is an emerging standard for representing mathematical objects with their semantics, allowing them to be exchanged between computer programs, stored in databases, or published on the worldwide web. While the original designers were mainly developers of computer algebra systems, it is now attracting interest from other areas of scientific computation and from many publishers of electronic documents with a significant mathematical content. There is a strong relationship to the MathML recommendation from the Worldwide Web Consortium, and a large overlap between the two developer communities.

OpenMath Content Dictionary (CD)

Content Dictionaries (CDs) are used to assign informal and formal semantics to all symbols used in the OpenMath objects. They define the symbols used to represent concepts arising in a particular area of mathematics.

The Content Dictionaries are public, they represent the actual common knowledge among OpenMath applications. Content Dictionaries fix the "meaning" of objects independently of the application. The application receiving the object may then recognize whether or not, according to the semantics of the symbols defined in the Content Dictionaries, the object can be transformed to the corresponding internal representation used by the application.

The original CDs for OpenMath were developed on the OpenMath project, and the MONET project has further developed this foundation. Originally the CDs and OpenMath objects were encoded using DTDs specifically developed for OpenMath. Monet has begun investigating the use of Semantic Web technologies in the OpenMath context. The example given takes part a CD for arithmetic operators, arith1 and re-encodes this using a RDFS vocabulary for all but the structures called "Formal Mathematical Properties". Syntactically these could have been encoded in RDFS also, however in that case their mathematical semantics would no longer be available. The idea is to investigate whether standard RDF-aware tools could then be used, for example for searching such information, and exploring relationships and dependencies between CDs.

The combined RDF/OpenMath CD fragment is given below. The original CD, and the DTD on which it is based, are attached in the Appendices section. It should be noted that this is work in progress, the MONET project is in progress and version two of the OpenMath standard is under development.

OpenMath CD in RDF and OpenMath XML

<!-- MONET IST-2001-34145                  -->
<!-- refactor CD arith1 as RDF/RDFS        -->

<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:dc    = "http://purl.org/dc/elements/1.1/"
  xmlns:om    = "http://www.openmath.org/"
  xmlns:omcd  = "http://www.openmath.org/CD#"
  xmlns:omcds  = "http://www.openmath.org/CDs/"
  xmlns:omcmps  = "http://www.openmath.org/CMPs/"
  xmlns:omfmps  = "http://www.openmath.org/FMPs/"
  xmlns:omexs   = "http://www.openmath.org/Examples/"
  xmlns:omcdsa1 = "http://www.openmath.org/CDs/arith1#"
  xmlns         = "http://www.openmath.org/lang/"
>

<!--declarations of the types to support the RDF encoding -->


<rdfs:Resource rdf:about="http://www.openmath.org/CD#CDType" rdf:type = "rdfs:Class">
  <rdfs:label xml:lang="en">CDType</rdfs:label>
  <rdfs:comment>
    Class declaration for use by RDF representations of OpenMath CDs.
  </rdfs:comment>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#CDSymbolType" rdf:type = "rdfs:Class">
  <rdfs:label xml:lang="en">CDSymbolType</rdfs:label>
  <rdfs:comment>
    Class declaration for use by RDF representations of OpenMath CD Symbols.
  </rdfs:comment>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#CDUses" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">CDUses</rdfs:label>
  <rdfs:comment>
    Property declaration for the CDUses relation.
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDType"/>
  <rdfs:range rdfs:Resource="http://www.openmath.org/CD#CDType"/>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#CDDefinition" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">CDDefinition</rdfs:label>
  <rdfs:comment>
    Property declaration for the CDDefinition relation, ie "this CD defines this symbol".
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDType"/>
  <rdfs:range rdfs:Resource="http://www.openmath.org/CD#CDSymbolType"/>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#CDStatus" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">CDStatus</rdfs:label>
  <rdfs:comment>
    Property declaration for the CDStatus .
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDType"/>
  <rdfs:range rdfs:Resource="rdfs:Literal"/>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#CDVersion" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">CDVersion</rdfs:label>
  <rdfs:comment>
    Property declaration for the CDVersion .
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDType"/>
  <rdfs:range rdfs:Resource="rdfs:Literal"/>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#CDRevision" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">CDRevision</rdfs:label>
  <rdfs:comment>
    Property declaration for the CDRevision .
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDType"/>
  <rdfs:range rdfs:Resource="rdfs:Literal"/>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#CMP" rdf:type = "rdfs:Class">
  <rdfs:label xml:lang="en">CMP</rdfs:label>
  <rdfs:comment>
    Class declaration for a CMP (Commented Mathematical Property) .
        Declaring these as resources rather than literals allows them to be shared.
  </rdfs:comment>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#hasCMP" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">hasCMP</rdfs:label>
  <rdfs:comment>
    Property declaration for associated CMP (Commented Mathematical Property) .
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDSymbolType"/>
  <rdfs:range rdfs:Resource="http://www.openmath.org/CD#CMP"/>
</rdfs:Resource>


<rdfs:Resource rdf:about="http://www.openmath.org/CD#FMP" rdf:type = "rdfs:Class">
  <rdfs:label xml:lang="en">FMP</rdfs:label>
  <rdfs:comment>
    Class declaration for use by RDF representations of OpenMath FMPs.
  </rdfs:comment>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#hasFMP" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">hasFMP</rdfs:label>
  <rdfs:comment>
    Property declaration for associated FMP (Formal Mathematical Property) .
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDSymbolType"/>
  <rdfs:range rdfs:Resource="http://www.openmath.org/CD#FMP"/>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#FMPUses" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">FMPUses</rdfs:label>
  <rdfs:comment>
    Property declaration for the FMPUses relation.
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#FMP"/>
  <rdfs:range rdfs:Resource="http://www.openmath.org/CD#CDType"/>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#Example" rdf:type = "rdfs:Class">
  <rdfs:label xml:lang="en">Example</rdfs:label>
  <rdfs:comment>
    Class declaration for use by RDF representations of OpenMath Examples.
  </rdfs:comment>
</rdfs:Resource>

<rdfs:Resource rdf:about="http://www.openmath.org/CD#hasExample" rdf:type = "rdfs:Property">
  <rdfs:label xml:lang="en">hasExample</rdfs:label>
  <rdfs:comment>
    Property declaration for associated Example .
  </rdfs:comment>
  <rdfs:domain rdfs:Resource="http://www.openmath.org/CD#CDSymbolType"/>
  <rdfs:range rdfs:Resource="http://www.openmath.org/CD#Example"/>
</rdfs:Resource>



<!-- the CD arith1  -->

<rdfs:Resource rdf:type ="http://www.openmath.org/CD#CDType" rdf:about ="http://www.openmath.org/CDs/arith1">
  <dc:title>CD-Arith1</dc:title>
  <dc:publisher>The OpenMath Society</dc:publisher>
  <dc:description>This CD defines symbols for common arithmetic functions.</dc:description>
  <dc:aboutentifier>omcds:arith1</dc:aboutentifier>
  <dc:date>2001-03-12</dc:date>
  <rdfs:comment>
    declares a resource which represents the OM arith1 CD. Generic metadata in Dublin Core.
  </rdfs:comment>
</rdfs:Resource>

<omcds:arith1 omcd:CDStatus = "official" />
<omcds:arith1 omcd:CDRevision = "0" />
<omcds:arith1 omcd:CDVersion = "2" />

<!-- (possibly) shared CMPs  -->

<rdfs:Resource rdf:type ="http://www.openmath.org/CD#CMP" rdf:about ="http://www.openmath.org/CMPs/CMP-CDarith1-1">
  <rdf:value>lcm(a,b) = a*b/gcd(a,b)</rdf:value>
  <dc:description>This CMP relates the lcm and gcd symbols.
  </dc:description>
</rdfs:Resource>

<rdfs:Resource rdf:type ="http://www.openmath.org/CD#CMP" rdf:about ="http://www.openmath.org/CMPs/CMP-CDarith1-2">
  <rdf:value>for all integers a,b | There does not exist a c > 0 such that c/a is an Integer and c/b is an
              Integer and lcm(a,b) > c. Note that this implies that gcd(a,b) > 0
  </rdf:value>
  <dc:description>This CMP relates to the lcm symbol.
  </dc:description>
</rdfs:Resource>



<!-- lcm, a symbol -->

<omcds:arith1 omcd:CDDefinition ="http://www.openmath.org/CDs/arith1#lcm" />

<rdfs:Resource rdf:type ="http://www.openmath.org/CD#CDSymbolType" rdf:about ="http://www.openmath.org/CDs/arith1#lcm">
  <dc:description>The symbol to represent the n-ary function to return the least common
     multiple of its arguments.
  </dc:description>
</rdfs:Resource>

<omcdsa1:lcm omcd:hasCMP ="http://www.openmath.org/CMPs/CMP-CDarith1-1" />
<omcdsa1:lcm omcd:hasCMP ="http://www.openmath.org/CMPs/CMP-CDarith1-2" />

<omcdsa1:lcm omcd:hasFMP ="http://www.openmath.org/FMPs/FMP-CDarith1-1" />
<omcdsa1:lcm omcd:hasFMP ="http://www.openmath.org/FMPs/FMP-CDarith1-2" />


<!-- gcd, a symbol -->

<omcds:arith1 omcd:CDDefinition ="http://www.openmath.org/CDs/arith1#gcd" />

<rdfs:Resource rdf:type ="http://www.openmath.org/CD#CDSymbolType" rdf:about ="http://www.openmath.org/CDs/arith1#gcd">
  <dc:description> The symbol to represent the n-ary function to return the gcd (greatest
                   common divisor) of its arguments.
  </dc:description>
</rdfs:Resource>

<omcdsa1:gcd omcd:hasCMP ="http://www.openmath.org/CMPs/CMP1" />

<omcdsa1:lcm omcd:hasFMP ="http://www.openmath.org/FMPs/FMP-CDarith1-1" />
<omcdsa1:lcm omcd:hasFMP ="http://www.openmath.org/FMPs/FMP-CDarith1-3" />

<omcdsa1:lcm omcd:hasExample = "http://www.openmath.org/Examples/Example-CDarith1-1" />



<!--declarations of the FMPs to support the RDF encoding of CD arith1 -->


<rdfs:Resource rdf:type ="http://www.openmath.org/CD#FMP" rdf:about ="http://www.openmath.org/FMPs/FMP-CDarith1-1">
<dc:description> lcm(a,b) = a*b/gcd(a,b)</dc:description>
<rdf:value rdf:parseType="Literal" >
<FMP>
<om:OMOBJ>
  <om:OMA>
    <om:OMS om:cd="relation1" om:name="eq"/>
    <om:OMZ>
      <om:OMS om:cd="arith1" om:name="lcm"/>
      <om:OMV om:name="a"/>
      <om:OMV om:name="b"/>
    </om:OMZ>
    <om:OMA>
      <om:OMS om:cd="arith1" om:name="divide"/>
      <om:OMA>
        <om:OMS om:cd="arith1" om:name="times"/>
        <om:OMV om:name="a"/>
        <om:OMV om:name="b"/>
      </om:OMA>
      <om:OMA>
        <om:OMS om:cd="arith1" om:name="gcd"/>
        <om:OMV om:name="a"/>
        <om:OMV om:name="b"/>
      </om:OMA>
    </om:OMA>
  </om:OMA>
</om:OMOBJ>
</FMP>
</rdf:value>
</rdfs:Resource>


<rdfs:Resource rdf:type ="http://www.openmath.org/CD#FMP" rdf:about ="http://www.openmath.org/FMPs/FMP-CDarith1-2">
<dc:description>
for all integers a,b |
There does not exist a c > 0 such that c/a is an Integer and c/b is an
Integer and lcm(a,b) > c.
</dc:description>
<rdf:value rdf:parseType="Literal" >
<FMP>
<om:OMOBJ>
<om:OMBIND>
  <om:OMS om:cd="quant1" om:name="forall"/>
  <om:OMBVAR>
    <om:OMV om:name="a"/>
    <om:OMV om:name="b"/>
  </om:OMBVAR>
  <om:OMA>
    <om:OMS om:cd="logic1" om:name="implies"/>
    <om:OMA>
      <om:OMS om:cd="logic1" om:name="and"/>
      <om:OMA>
        <om:OMS om:cd="set1" om:name="in"/>
        <om:OMV om:name="a"/>
        <om:OMS om:cd="setname1" om:name="Z"/>
      </om:OMA>
      <om:OMA>
        <om:OMS om:cd="set1" om:name="in"/>
        <om:OMV om:name="b"/>
        <om:OMS om:cd="setname1" om:name="Z"/>
      </om:OMA>
    </om:OMA>
    <om:OMA>
      <om:OMS om:cd="logic1" om:name="not"/>
      <om:OMBIND>
        <om:OMS om:cd="quant1" om:name="exists"/>
        <om:OMBVAR>
          <om:OMV om:name="c"/>
        </om:OMBVAR>
        <om:OMA>
          <om:OMS om:cd="logic1" om:name="and"/>
          <om:OMA>
            <om:OMS om:cd="relation1" om:name="gt"/>
              <om:OMV om:name="c"/>
              <om:OMI>0</om:OMI>
          </om:OMA>
          <om:OMA>
            <om:OMS om:cd="integer1" om:name="factorof"/>
              <om:OMV om:name="a"/>
              <om:OMV om:name="c"/>
          </om:OMA>
          <om:OMA>
            <om:OMS om:cd="integer1" om:name="factorof"/>
              <om:OMV om:name="b"/>
              <om:OMV om:name="c"/>
          </om:OMA>
          <om:OMA>
            <om:OMS om:cd="relation1" om:name="lt"/>
            <om:OMV om:name="c"/>
            <om:OMA>
              <om:OMS om:cd="arith1" om:name="lcm"/>
              <om:OMV om:name="a"/>
              <om:OMV om:name="b"/>
            </om:OMA>
          </om:OMA>
        </om:OMA>
      </om:OMBIND>
    </om:OMA>
  </om:OMA>
</om:OMBIND>
</om:OMOBJ>
</FMP>
</rdf:value>
</rdfs:Resource>

<rdfs:Resource rdf:type ="http://www.openmath.org/CD#FMP" rdf:about ="http://www.openmath.org/FMPs/FMP-CDarith1-3">
<dc:description>
for all integers a,b |
There does not exist a c such that a/c is an Integer and b/c is an
Integer and c > gcd(a,b).
Note that this implies that gcd(a,b) > 0
</dc:description>
<rdf:value rdf:parseType="Literal" >
<FMP>
<om:OMOBJ>
<om:OMBIND>
  <om:OMS om:cd="quant1" om:name="forall"/>
  <om:OMBVAR>
    <om:OMV om:name="a"/>
    <om:OMV om:name="b"/>
  </om:OMBVAR>
  <om:OMA>
    <om:OMS om:cd="logic1" om:name="implies"/>
    <om:OMA>
      <om:OMS om:cd="logic1" om:name="and"/>
      <om:OMA>
        <om:OMS om:cd="set1" om:name="in"/>
        <om:OMV om:name="a"/>
        <om:OMS om:cd="setname1" om:name="Z"/>
      </om:OMA>
      <om:OMA>
        <om:OMS om:cd="set1" om:name="in"/>
        <om:OMV om:name="b"/>
        <om:OMS om:cd="setname1" om:name="Z"/>
      </om:OMA>
    </om:OMA>
    <om:OMA>
      <om:OMS om:cd="logic1" om:name="not"/>
      <om:OMBIND>
        <om:OMS om:cd="quant1" om:name="exists"/>
        <om:OMBVAR>
          <om:OMV om:name="c"/>
        </om:OMBVAR>
        <om:OMA>
          <om:OMS om:cd="logic1" om:name="and"/>
          <om:OMA>
            <om:OMS om:cd="set1" om:name="in"/>
            <om:OMA>
              <om:OMS om:cd="arith1" om:name="divide"/>
              <om:OMV om:name="a"/>
              <om:OMV om:name="c"/>
            </om:OMA>
            <om:OMS om:cd="setname1" om:name="Z"/>
          </om:OMA>
          <om:OMA>
            <om:OMS om:cd="set1" om:name="in"/>
            <om:OMA>
              <om:OMS om:cd="arith1" om:name="divide"/>
              <om:OMV om:name="b"/>
              <om:OMV om:name="c"/>
            </om:OMA>
            <om:OMS om:cd="setname1" om:name="Z"/>
          </om:OMA>
          <om:OMA>
            <om:OMS om:cd="relation1" om:name="gt"/>
            <om:OMV om:name="c"/>
            <om:OMA>
              <om:OMS om:cd="arith1" om:name="gcd"/>
              <om:OMV om:name="a"/>
              <om:OMV om:name="b"/>
            </om:OMA>
          </om:OMA>
        </om:OMA>
      </om:OMBIND>
    </om:OMA>
  </om:OMA>
</om:OMBIND>
</om:OMOBJ>
</FMP>
</rdf:value>
</rdfs:Resource>

<rdfs:Resource rdf:type ="http://www.openmath.org/CD#Example" rdf:about = "http://www.openmath.org/Examples/Example-CDarith1-1">
<dc:description>
gcd(6,9) = 3
</dc:description>
<rdf:value rdf:parseType="Literal" >
<Example>
<om:OMOBJ>
  <om:OMA>
    <om:OMS om:cd="relation1" om:name="eq"/>
    <om:OMA>
      <om:OMS om:cd="arith1" om:name="gcd"/>
      <om:OMI> 6 </om:OMI>
      <om:OMI> 9 </om:OMI>
    </om:OMA>
    <om:OMI> 3 </om:OMI>
  </om:OMA>
</om:OMOBJ>
</Example>
</rdf:value>
</rdfs:Resource>



</rdf:RDF>

References

Appendices

OpenMath CD in OpenMath XML

<CD>
<CDName> arith1 </CDName>
<CDURL> http://www.openmath.org/cd/arith1.ocd </CDURL>
<CDReviewDate> 2003-04-01 </CDReviewDate>
<CDStatus> official </CDStatus>
<CDDate> 2001-03-12 </CDDate>
<CDVersion> 2 </CDVersion>
<CDRevision> 0 </CDRevision>
<CDUses>
  <CDName>alg1</CDName>
  <CDName>fns1</CDName>
  <CDName>integer1</CDName>
  <CDName>interval1</CDName>
  <CDName>linalg2</CDName>
  <CDName>logic1</CDName>
  <CDName>quant1</CDName>
  <CDName>relation1</CDName>
  <CDName>set1</CDName>
  <CDName>setname1</CDName>
  <CDName>transc1</CDName>
</CDUses>

<Description> 
This CD defines symbols for common arithmetic functions.
</Description>

<CDDefinition>
<Name> lcm </Name>
<Description> 
The symbol to represent the n-ary function to return the least common
multiple of its arguments.
</Description>

<CMP> lcm(a,b) = a*b/gcd(a,b) </CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS cd="arith1" name="lcm"/>
      <OMV name="a"/>
      <OMV name="b"/>
    </OMA>
    <OMA>
      <OMS cd="arith1" name="divide"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
            <OMV name="a"/>
            <OMV name="b"/>
      </OMA>
      <OMA>
        <OMS cd="arith1" name="gcd"/>
        <OMV name="a"/>
        <OMV name="b"/>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>
</FMP>
<CMP>
for all integers a,b |
There does not exist a c>0 such that c/a is an Integer and c/b is an
Integer and lcm(a,b) > c.
</CMP>

<FMP>
<OMOBJ>
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="a"/>
    <OMV name="b"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMV name="a"/>
        <OMS cd="setname1" name="Z"/>
      </OMA>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMV name="b"/>
        <OMS cd="setname1" name="Z"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
        <OMBVAR>
          <OMV name="c"/>
        </OMBVAR>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="relation1" name="gt"/>
              <OMV name="c"/>
              <OMI>0</OMI>
          </OMA>
          <OMA>
            <OMS cd="integer1" name="factorof"/>
              <OMV name="a"/>
              <OMV name="c"/>
          </OMA>
          <OMA>
            <OMS cd="integer1" name="factorof"/>
              <OMV name="b"/>
              <OMV name="c"/>
          </OMA>
          <OMA>
            <OMS cd="relation1" name="lt"/>
            <OMV name="c"/>
            <OMA>
              <OMS cd="arith1" name="lcm"/>
              <OMV name="a"/>
              <OMV name="b"/>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>
</FMP>
</CDDefinition>

<CDDefinition>
<Name> gcd </Name>
<Description> 
The symbol to represent the n-ary function to return the gcd (greatest
common divisor) of its arguments.
</Description>

<CMP>
for all integers a,b |
There does not exist a c such that a/c is an Integer and b/c is an
Integer and c > gcd(a,b).

Note that this implies that gcd(a,b) > 0
</CMP>

<FMP>
<OMOBJ>
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMV name="a"/>
    <OMV name="b"/>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMV name="a"/>
        <OMS cd="setname1" name="Z"/>
      </OMA>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMV name="b"/>
        <OMS cd="setname1" name="Z"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="not"/>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
        <OMBVAR>
          <OMV name="c"/>
        </OMBVAR>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMA>
              <OMS cd="arith1" name="divide"/>
              <OMV name="a"/>
              <OMV name="c"/>
            </OMA>
            <OMS cd="setname1" name="Z"/>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMA>
              <OMS cd="arith1" name="divide"/>
              <OMV name="b"/>
              <OMV name="c"/>
            </OMA>
            <OMS cd="setname1" name="Z"/>
          </OMA>
          <OMA>
            <OMS cd="relation1" name="gt"/>
            <OMV name="c"/>
            <OMA>
              <OMS cd="arith1" name="gcd"/>
              <OMV name="a"/>
              <OMV name="b"/>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>
</FMP>

<Example>
gcd(6,9) = 3
<OMOBJ>
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS cd="arith1" name="gcd"/>
      <OMI> 6 </OMI>
      <OMI> 9 </OMI>
    </OMA>
    <OMI> 3 </OMI>
  </OMA>
</OMOBJ>
</Example>
</CDDefinition>

</CD>

DTD for the OpenMath CD

<!-- omcd.dtd -->
<!-- ********************************************* -->
<!--                                               -->
<!-- DTD for OpenMath CD                           -->
<!-- (c) EP24969 the ESPRIT OpenMath Consortium    -->
<!-- date = 28.aug.1998                            -->
<!-- author = s.buswell sb@stilo.demon.co.uk       -->
<!--                                               -->
<!-- edited by n.howgrave-graham 30.aug.98         -->
<!-- edited by sb 4.sep.98                         -->
<!-- edited by nh-g 4.sep.98                       -->
<!-- edited by sb 1.nov.98                         -->
<!-- edited by sb 1.nov.98                         -->
<!-- edited by dpc 1999-04-13                      -->
<!-- edited by dpc 1999-05-11  CDDate & CDVersion  -->
<!-- edited by dpc 1999-06-21  Delete Signature & Presentation  -->
<!--                           Force Name to be first child of -->
<!--                           CDDefinition -->
<!--                                               -->
<!--                                               -->
<!-- ********************************************* -->
<!ELEMENT CDComment      (#PCDATA) >
<!ELEMENT CDName         (#PCDATA) >
<!ELEMENT CDURL          (#PCDATA) >
<!ELEMENT CDUses         (CDName)*  >
<!ENTITY % inhel        "(#PCDATA)" >
<!ENTITY % inhel2       "(#PCDATA | OMOBJ)*" >
<!ELEMENT CDReviewDate   %inhel; >
<!ELEMENT CDDate         %inhel; >
<!ELEMENT CDVersion      %inhel; >
<!ELEMENT CDRevision     %inhel; >
<!ELEMENT CDStatus       %inhel; >
<!ELEMENT Description    %inhel; >
<!ELEMENT Name           %inhel; >
<!ELEMENT CMP            %inhel; >
<!-- include dtd for OM objects -->
<!ENTITY  % omobjectdtd SYSTEM "omobj.dtd" >
%omobjectdtd;
<!ELEMENT FMP            (OMOBJ) >             <!-- embedded OM -->
<!ELEMENT Example        %inhel2; >
<!ELEMENT CDDefinition    (Name, Description,
                          (CDComment | Example | FMP | CMP )*) >
<!ELEMENT CD             (CDComment | CDName | Description |
                         CDReviewDate | CDDate |CDVersion |CDRevision |
                         CDStatus | CDURL | CDUses | CDDefinition |
Example)* >
<!-- end of DTD for OM CD -->