@base <http://km.aifb.kit.edu/projects/numbers/number> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix : <#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix cc: <http://creativecommons.org/ns#> .

<>
    cc:license <http://creativecommons.org/publicdomain/zero/1.0/> ;
    a owl:Ontology .

:Integer
    a owl:Class ;
    rdfs:comment """
      A number that can be written without requiring a fractional or decimal
      part.
    """@en ;
    rdfs:label "Ganze Zahl"@de, "Integer"@en, "Z" ;
    rdfs:subClassOf :Number, [
        a owl:Restriction ;
        owl:onProperty :previous ;
        owl:someValuesFrom :Integer
    ], [
        a owl:Restriction ;
        owl:onProperty :next ;
        owl:someValuesFrom :Integer
    ] .

:NaturalNumber
    a owl:Class ;
    rdfs:comment """
      A positive integer, i.e. a number greater than zero that can be written
      without requiring fractional or decimal components.
    """@en ;
    rdfs:label "N", "Natürliche Zahl"@de, "Number"@en ;
    rdfs:subClassOf :Integer, :PositiveNumber .

:Number
    a owl:Class ;
    rdfs:comment """
      A mathemtical object used in counting and measuring.
    """@en ;
    rdfs:label "Number"@en, "Zahl"@de .

:PositiveNumber
    a owl:Class ;
    rdfs:comment "All numbers bigger than 0."@en ;
    rdfs:label "0", "Positive Zahl"@de, "Positive number"@en ;
    rdfs:subClassOf :Number ;
    owl:equivalentClass [
        a owl:Restriction ;
        owl:onProperty :greaterThan ;
        owl:someValuesFrom [
            a owl:Class ;
            owl:oneOf (:n0
            )
        ]
    ] .

:Prime
    a owl:Class ;
    rdfs:comment """
      A number with no factors but itself and 1.
    """@en ;
    rdfs:label "Prime number"@en, "Primzahl"@de ;
    rdfs:subClassOf :NaturalNumber, [
        a owl:Restriction ;
        owl:cardinality """
          1
        """^^xsd:int ;
        owl:onProperty :primefactor
    ] .

:digitsum
    a owl:ObjectProperty ;
    rdfs:comment """
      The sum of the individual digits of this number in Base 10.
    """@en ;
    rdfs:domain :NaturalNumber ;
    rdfs:label "Digit sum"@en, "Quersumme"@de ;
    rdfs:range :NaturalNumber .

:greaterThan
    a owl:ObjectProperty, owl:TransitiveProperty ;
    rdfs:comment """
      A number that is smaller than the given one, i.e. 5 greaterThan 3.
    """@en ;
    rdfs:domain :Number ;
    rdfs:label ">", "greater than"@en, "größer als"@de ;
    rdfs:range :Number ;
    owl:inverseOf :lessThan .

:lessThan
    a owl:ObjectProperty, owl:TransitiveProperty ;
    rdfs:comment """
      A number that is bigger than the given one, e.g. 8 lessThan 5 is correct.
    """@en ;
    rdfs:domain :Number ;
    rdfs:label "<", "kleiner als"@de, "less than"@en ;
    rdfs:range :Number ;
    owl:inverseOf :greaterThan .

:log
    a owl:DatatypeProperty ;
    rdfs:comment """
      A number quite close to the natural logarithm of the given value.
    """@en ;
    rdfs:domain :PositiveNumber ;
    rdfs:label "Natural logarithm"@en, "Natürlicher Logarithmus"@de, "ln" ;
    rdfs:range xsd:float .

:n0
    :value "0"^^xsd:int ;
    a :Integer ;
    rdf:value "0"^^xsd:int ;
    rdfs:comment """
      The number 0, i.e. the neutral element on Addition.
    """@en ;
    rdfs:label "0", "Null"@de, "Zero"@en .

:next
    a owl:FunctionalProperty, owl:InverseFunctionalProperty, owl:ObjectProperty ;
    rdfs:comment """
      The number that is the sucessor of a  number.
    """@en ;
    rdfs:domain :Integer ;
    rdfs:label "+1", "Nachfolger"@de, "Successor"@en ;
    rdfs:range :Integer ;
    rdfs:subPropertyOf :lessThan ;
    owl:inverseOf :previous .

:previous
    a owl:FunctionalProperty, owl:InverseFunctionalProperty, owl:ObjectProperty ;
    rdfs:comment """
      The number that is predecessing this one.
    """@en ;
    rdfs:domain :Integer ;
    rdfs:label "-1", "Predecessor"@en, "Vorgänger"@de ;
    rdfs:range :Integer ;
    rdfs:subPropertyOf :greaterThan ;
    owl:inverseOf :next .

:primefactor
    a owl:ObjectProperty ;
    rdfs:comment """
      A factor of the number that is a prime at the same time.
    """@en ;
    rdfs:domain :NaturalNumber ;
    rdfs:label "Prime factor"@en, "Primfaktor"@de ;
    rdfs:range :Prime .

:roman
    a owl:DatatypeProperty, owl:FunctionalProperty ;
    rdfs:comment """
      The roman literal representing the number.
    """@en ;
    rdfs:domain :NaturalNumber ;
    rdfs:label "Roman literal"@en, "Römische Zahl"@de ;
    rdfs:range xsd:string .

:value
    a owl:DatatypeProperty, owl:FunctionalProperty ;
    rdfs:comment """
      Connects an integer individual with the integer literal. In OWL Full
      one may state that this property is a subproperty of owl:sameAs, and
      thus that the individuals and the literals are denoting the same 
      entity.
    """@en ;
    rdfs:domain :Integer ;
    rdfs:label "Value"@en, "Wert"@de ;
    rdfs:range xsd:int .