(:name Type-axiom-1
 :description " Relation 'Type' holds for objects S and O if and only if relation 'PropertyValue' holds for objects 'type', S, and O."
 :body (<=> (Type ?s ?o) (PropertyValue type3 ?s ?o)))


(:name FunctionalProperty-axiom-1
 :description " An object FP is 'FunctionalProperty' if and only if FP is type 'Property' and if objects V1 and V2 are both values of FP for some object, then V1 is equal to V2.  (I.e., functional properties are those properties that are functional in their values.)"
 :body (<=> (FunctionalProperty ?fp)
        (and (Type ?fp rdf\:Property)
         (forall (?s ?v1 ?v2)
          (=>
           (and (PropertyValue ?fp ?s ?v1) (PropertyValue ?fp ?s ?v2))
           (= ?v1 ?v2))))))


(:name DisjointAll-axiom-1
 :description " An object L is 'DisjointAll' if and only if L is type 'List' and when L has a value F for property 'first' and a value R for property 'rest' then F is disjoint from every C that is a value of 'item' for R and R is 'DisjointAll'.  (I.e., a list L is 'DisjointAll' if and only each pair of its items is disjoint.)"
 :body (<=> (DisjointAll ?l)
        (and (Type ?l daml\:List)
         (or (= ?l daml\:nil)
          (forall (?f ?r)
           (=>
            (and (PropertyValue daml\:first ?l ?f)
             (PropertyValue daml\:rest ?l ?r))
            (and
             (forall (?c)
              (=> (PropertyValue daml\:item ?r ?c)
               (PropertyValue daml\:disjointWith ?f ?c)))
             (DisjointAll ?r))))))))


(:name NoRepeatsList-axiom-1
 :description " A 'NoRepeatsList' is a list for which no item occurs more than once."
 :body (<=> (NoRepeatsList ?l)
        (or (= ?l daml\:nil) (exists (?x) (= ?l (listof ?x)))
         (and (not (daml\:item (daml\:rest ?l) (daml\:first ?l)))
          (NoRepeatsList (daml\:rest ?l))))))


(:name Resource-axiom-1
 :description " 'Resource' is type 'Class'."
 :body (Type rdfs\:Resource rdfs\:Class))


(:name Property-axiom-1
 :description " The first argument of relation 'PropertyValue' is type 'Property'."
 :body (=> (PropertyValue ?p ?s ?o) (Type ?p rdf\:Property)))


(:name Class-axiom-1
 :description " No object can be both type 'Property' and type 'Class' (i.e., properties and RDF-S classes are disjoint)."
 :body (not (and (Type ?x rdf\:Property) (Type ?x rdfs\:Class))))


(:name Literal-axiom-1
 :description " 'Literal' is type 'Class'."
 :body (Type Literal rdfs\:Class))


(:name Statement-axiom-1
 :description " If an object ST is type 'Statement', then there exists a value of 'predicate' for ST, a value of 'subject' for ST, and a value of 'object' for ST. (I.e., every statement has a predicate, subject, and object.)"
 :body (=> (Type ?st rdf\:Statement)
        (exists (?p ?r ?o)
         (and (PropertyValue rdf\:predicate ?st ?p)
          (PropertyValue rdf\:subject ?st ?r)
          (PropertyValue rdf\:object ?st ?o)))))


(:name Container-axiom-1
 :description " If an object C is type 'Container', then C is a KIF list.  (I.e., a container is considered to be a list as defined in KIF.)"
 :body (=> (Type ?c rdf\:Container) (daml\:List ?c)))


(:name Container-axiom-2
 :description " An object C is type 'Container' if and only if C is type 'Bag' or type 'Seq' or type 'Alt'.  (I.e., a container is a bag, a sequence, or an alternative.)"
 :body (<=> (Type ?c rdf\:Container)
        (or (Type ?c rdf\:Bag) (Type ?c rdf\:Seq) (Type ?c rdf\:Alt))))


(:name ContainerMembershipProperty-axiom-1
 :description " If an object C is type 'ContainerMembershipProperty', then C is also type 'Property'.  (I.e., a container membership property is a property.)"
 :body (=> (Type ?c rdf\:ContainerMembershipProperty)
        (Type ?c rdf\:Property)))


(:name type-axiom-1
 :description " 'type' is type 'Property'.  (I.e., 'type' is a property.)"
 :body (Type rdf\:type rdf\:Property))


(:name type-axiom-2
 :description " The first argument of 'Type' is a resource and the second argument of 'Type' is a class."
 :body (=> (Type ?r ?c)
        (and (Type ?r rdfs\:Resource) (Type ?c rdfs\:Class))))


(:name subject-axiom-1
 :description " 'subject' is 'FunctionalProperty', and if an object SB is the value of 'subject' for an object ST, then ST is type 'Statement' and SB is type 'Resource'.  (I.e., every statement has exactly one subject, and that subject is a resource.)"
 :body (FunctionalProperty rdf\:subject))


(:name subject-axiom-2
 :description " 'subject' is 'FunctionalProperty', and if an object SB is the value of 'subject' for an object ST, then ST is type 'Statement' and SB is type 'Resource'.  (I.e., every statement has exactly one subject, and that subject is a resource.)"
 :body (=> (PropertyValue rdf\:subject ?st ?sb)
        (and (Type ?st rdf\:Statement) (Type ?sb rdfs\:Resource))))


(:name predicate-axiom-1
 :description " 'predicate' is 'FunctionalProperty', and if an object P is the value of 'predicate' for an object ST, then P is type 'Property' and ST is type 'Statement'.  (I.e., every statement has exactly one predicate, and that predicate is a property.)"
 :body (FunctionalProperty rdf\:predicate))


(:name predicate-axiom-2
 :description " 'predicate' is 'FunctionalProperty', and if an object P is the value of 'predicate' for an object ST, then P is type 'Property' and ST is type 'Statement'.  (I.e., every statement has exactly one predicate, and that predicate is a property.)"
 :body (=> (PropertyValue rdf\:predicate ?st ?p)
        (and (Type ?st rdf\:Statement) (Type ?p rdf\:Property))))


(:name object-axiom-1
 :description " 'object' is 'FunctionalProperty', and if an object O is the value of 'object' for an object ST, then O is type 'Resource' and ST is type 'Statement'.  (I.e., every statement has exactly one object, and that object is a resource.)"
 :body (FunctionalProperty rdf\:object))


(:name object-axiom-2
 :description " 'object' is 'FunctionalProperty', and if an object O is the value of 'object' for an object ST, then O is type 'Resource' and ST is type 'Statement'.  (I.e., every statement has exactly one object, and that object is a resource.)"
 :body (=> (PropertyValue rdf\:object ?st ?o)
        (and (Type ?st rdf\:Statement) (Type ?o rdfs\:Resource))))


(:name value-axiom-1
 :description " 'value' is type 'Property', and if an object V is a value of 'value' for an object SV, then SV and V are each type 'Resource'."
 :body (Type rdf\:value rdf\:Property))


(:name value-axiom-2
 :description " 'value' is type 'Property', and if an object V is a value of 'value' for an object SV, then SV and V are each type 'Resource'."
 :body (=> (PropertyValue rdf\:value ?sv ?v)
        (and (Type ?sv rdfs\:Resource) (Type ?v rdfs\:Resource))))


(:name _N-axiom-1
 :description " For each positive integer N, '_N' is 'FunctionalProperty', and if an object O is the value of '_N' for an object C, then C is type 'Container'.  (The _N of a container is intended to be the Nth element of that container.)"
 :body (FunctionalProperty rdf\:_1))


(:name _N-axiom-2
 :description " For each positive integer N, '_N' is 'FunctionalProperty', and if an object O is the value of '_N' for an object C, then C is type 'Container'.  (The _N of a container is intended to be the Nth element of that container.)"
 :body (=> (PropertyValue rdf\:_1 ?c ?o) (Type ?c rdf\:Container)))


(:name ConstraintResource-axiom-1
 :description " 'Resource' is a value of 'subClassOf' for 'ConstraintResource'.  (I.e., a constraint resource is a resource.)"
 :body (PropertyValue subClassOf rdfs\:ConstraintResource
        rdfs\:Resource))


(:name ConstraintProperty-axiom-1
 :description " An object CP is type 'ConstraintProperty' if and only if it is type 'ConstraintResource' and type 'Property'.  (I.e., constraint properties are exactly those constraint resources that are also properties.)"
 :body (<=> (Type ?cp rdfs\:ConstraintProperty)
        (and (Type ?cp rdfs\:ConstraintResource)
         (Type ?cp rdf\:Property))))


(:name NonNegativeInteger-axiom-1
 :description " An object of type 'NonNegativeInteger' is an integer."
 :body (=> (Type ?n rdfs\:NonNegativeInteger) (Integer ?n)))


(:name subClassOf-axiom-1
 :description " 'subClassOf' is type 'Property'."
 :body (Type subClassOf rdf\:Property))


(:name subClassOf-axiom-2
 :description " An object CSUPER is a value of 'subClassOf' for an object CSUB if and only if CSUPER is type 'Class', CSUB is type 'Class', CSUB is not CSUPER, and if an object X is type CSUB then it is also type CSUPER.  (I.e., the arguments of subClassOf are classes, and objects in a subclass are also in the superclass.)"
 :body (<=> (PropertyValue subClassOf ?csub ?csuper)
        (and (Type ?csub rdfs\:Class) (Type ?csuper rdfs\:Class)
         (forall (?x) (=> (Type ?x ?csub) (Type ?x ?csuper))))))


(:name subPropertyOf-axiom-1
 :description " An object SUPERP is a value of 'subPropertyOf' of an object SUBP if and only if SUBP is type 'Property', SUPERP is type 'Property', and if an object V is a value of SUBP for an object O then V is also a value of SUPERP for O.  (I.e., if a subProperty has a value V for an object O, then the superproperty also has value V for O.)"
 :body (<=> (PropertyValue subPropertyOf ?subP ?superP)
        (and (Type ?subP rdf\:Property) (Type ?superP rdf\:Property)
         (forall (?o ?v)
          (=> (PropertyValue ?subP ?o ?v)
           (PropertyValue ?superP ?o ?v))))))


(:name seeAlso-axiom-1
 :description " 'Resource' is a value of both 'domain' and 'range' for 'seeAlso.  (I.e., 'seeAlso' is a property whose arguments are resources.)"
 :body (PropertyValue rdfs\:domain rdfs\:seeAlso rdfs\:Resource))


(:name seeAlso-axiom-2
 :description " 'Resource' is a value of both 'domain' and 'range' for 'seeAlso.  (I.e., 'seeAlso' is a property whose arguments are resources.)"
 :body (PropertyValue rdfs\:range rdfs\:seeAlso rdfs\:Resource))


(:name isDefinedBy-axiom-1
 :description " 'seeAlso' is a value of 'subPropertyOf' for 'isDefinedBy'.  (I.e., 'isDefinedBy' is a subproperty of 'seeAlso'.)"
 :body (PropertyValue subPropertyOf rdfs\:isDefinedBy rdfs\:seeAlso))


(:name comment-axiom-1
 :description " 'Literal' is the value of 'range' for 'comment'.  (I.e., 'comment' is a property whose value is a literal.)"
 :body (PropertyValue rdfs\:range rdfs\:comment Literal))


(:name label-axiom-1
 :description " 'Literal' is the value of 'range' for 'label'.  (I.e., 'label' is a property whose value is a literal.)"
 :body (PropertyValue rdfs\:range rdfs\:label Literal))


(:name ConstraintProperty-axiom-1
 :description " 'Property' is a value of 'subClassOf' for 'ConstraintProperty'.  (I.e., a constraint property is a property.)"
 :body (PropertyValue subClassOf rdfs\:ConstraintProperty
        rdf\:Property))


(:name range-axiom-1
 :description " 'range' is type 'ConstraintProperty' and 'FunctionalProperty'."
 :body (Type rdfs\:range rdfs\:ConstraintProperty))


(:name range-axiom-2
 :description " 'range' is type 'ConstraintProperty' and 'FunctionalProperty'."
 :body (FunctionalProperty rdfs\:range))


(:name range-axiom-3
 :description " An object R is the value of 'range' for an object P if and only if P is type 'Property', R is type 'Class', and if an object Y is a value of P then Y is type R.  (I.e., R is the range of P when P is a property, R is a class, and every value of P is an R.)"
 :body (<=> (PropertyValue rdfs\:range ?p ?r)
        (and (Type ?p rdf\:Property) (Type ?r rdfs\:Class)
         (forall (?x ?y) (=> (PropertyValue ?p ?x ?y) (Type ?y ?r))))))


(:name domain-axiom-1
 :description " 'domain' is type 'ConstraintProperty'."
 :body (Type rdfs\:domain rdfs\:ConstraintProperty))


(:name domain-axiom-2
 :description " If an object D is a value of 'domain' for an object P, then P is type 'Property', D is type 'Class', and if P has a value for an object X then X is type D.  (I.e., if D is a domain of P, then P is a property, D is a class, and every object that has a value of P is a D.)"
 :body (<=> (PropertyValue rdfs\:domain ?p ?d)
        (and (Type ?p rdf\:Property) (Type ?d rdfs\:Class)
         (forall (?x ?y) (=> (PropertyValue ?p ?x ?y) (Type ?x ?d))))))


(:name class-axiom-1
 :description " 'Class' is a subclass of 'Class'."
 :body (PropertyValue subClassOf rdfs\:Class rdfs\:Class))


(:name Datatype-axiom-1
 :description " 'Datatype' is a subclass of 'Class'."
 :body (PropertyValue subClassOf daml\:Datatype rdfs\:Class))


(:name Thing-axiom-1
 :description " 'Thing' is type 'Class'."
 :body (Type daml\:Thing rdfs\:Class))


(:name Thing-axiom-2
 :description " All objects X are type 'Thing'.  (I.e., 'Thing' is the class of all objects.)"
 :body (Type ?x daml\:Thing))


(:name Nothing-axiom-1
 :description " 'Nothing' is the value of 'complementOf' for 'Thing'.  (I.e., 'Nothing' is the complement of 'Thing'.)"
 :body (PropertyValue daml\:complementOf daml\:Thing daml\:Nothing))


(:name Restriction-axiom-1
 :description " 'Restriction' is a subclass of 'Class'."
 :body (PropertyValue subClassOf daml\:Restriction rdfs\:Class))


(:name AbstractProperty-axiom-1
 :description " 'Restriction' is a subclass of 'Class'."
 :body (PropertyValue subClassOf daml\:AbstractProperty rdf\:Property))


(:name DatatypeProperty-axiom-1
 :description " 'Restriction' is a subclass of 'Class'."
 :body (PropertyValue subClassOf daml\:DatatypeProperty rdfs\:Class))


(:name TransitiveProperty-axiom-1
 :description " An object P is type 'TransitiveProperty' if and only if P is type 'AbstractProperty' and if an object Y is a value of P for an object X and an object Z is a value of P for Y then Z is a value of P for X."
 :body (<=> (Type ?p daml\:TransitiveProperty)
        (and (Type ?p daml\:AbstractProperty)
         (forall (?x ?y ?z)
          (=> (and (PropertyValue ?p ?x ?y) (PropertyValue ?p ?y ?z))
           (PropertyValue ?p ?x ?z))))))


(:name UniqueProperty-axiom-1
 :description " An object P is type 'UniqueProperty' if and only if P is type 'Property' and if an object Y is a value of P for an object X and an object Z is a value of P for X then Y is equal to Z (i.e., then Y and Z are the same object)."
 :body (<=> (Type ?p daml\:UniqueProperty)
        (and (Type ?p rdf\:Property)
         (forall (?x ?y ?z)
          (=> (and (PropertyValue ?p ?x ?y) (PropertyValue ?p ?x ?z))
           (= ?y ?z))))))


(:name UnambiguousProperty-axiom-1
 :description " An object P is type 'UnambiguousProperty' if and only if P is type 'AbstractProperty' and if an object V is a value of P for an object X and V is a value of P for an object Y then X is equal to Y (i.e., then X and Y are the same object)."
 :body (<=> (Type ?p daml\:UnambiguousProperty)
        (and (Type ?p daml\:AbstractProperty)
         (forall (?x ?y ?v)
          (=> (and (PropertyValue ?p ?x ?v) (PropertyValue ?p ?y ?v))
           (= ?x ?y))))))


(:name List-axiom-1
 :description " 'Seq' is a value of 'subClassOf' for 'List'.  (I.e., lists are sequences.)"
 :body (PropertyValue subClassOf daml\:List rdf\:Seq))


(:name Ontology-axiom-1
 :description " An ontology is type 'Class'."
 :body (Type daml\:Ontology rdfs\:Class))


(:name equivalentTo-axiom-1
 :description " An object Y is a value of 'equivalentTo' for an object X if and only if X is equal to Y.  (I.e., saying that objects X and Y are 'equivalentTo' is logically equivalent to saying that X and Y denote the same object.)"
 :body (<=> (PropertyValue daml\:equivalentTo ?x ?y) (= ?x ?y)))


(:name sameClassAs-axiom-1
 :description " 'equivalentTo' is a value of 'subPropertyOf' for 'sameClassAs'.  (I.e., 'sameClassAs' is 'equivalentTo' for classes.)"
 :body (PropertyValue subPropertyOf daml\:sameClassAs
        daml\:equivalentTo))


(:name sameClassAs-axiom-2
 :description " C2 is a value of 'sameClassAs' for C1 if and only if C2 is a value of 'subClassOf' for C1 and C1 is a value of 'subClassOf' for C2."
 :body (<=> (PropertyValue daml\:sameClassAs ?c1 ?c2)
        (and (subClassOf ?c1 ?c2) (subClassOf ?c2 ?c1))))


(:name sameClassAs-axiom-3
 :description " If C1 is type 'Class' and C2 is a value of 'equivalentTo' for C1, then C2 is a value of 'sameClassAs' for C1 (i.e., if C1 is a class and C1 is equivalent to C2, then C1 is sameClassAs C2)."
 :body (=>
        (and (Type ?c1 rdfs\:Class)
         (PropertyValue daml\:equivalentTo ?c1 ?c2))
        (PropertyValue daml\:sameClassAs ?c1 ?c2)))


(:name samePropertyAs-axiom-1
 :description " 'equivalentTo' is a value of 'subPropertyOf' for 'samePropertyAs'.  (I.e., 'samePropertyAs' is 'equivalentTo' for properties.)"
 :body (PropertyValue subPropertyOf daml\:samePropertyAs
        daml\:equivalentTo))


(:name samePropertyAs-axiom-2
 :description " P2 is a value of 'samePropertyAs' for P1 if and only if P2 is a value of 'subPropertyOf' for P1 and P1 is a value of 'subPropertyOf' for P2."
 :body (<=> (PropertyValue daml\:samePropertyAs ?P1 ?P2)
        (and (subPropertyOf ?P1 ?P2) (subPropertyOf ?P2 ?P1))))


(:name samePropertyAs-axiom-3
 :description " If P1 is type 'Property' and P2 is a value of 'equivalentTo' for P1, then P2 is a value of 'samePropertyAs' for P1 (i.e., if P1 is a property and P1 is equivalent to P2, then P1 is samePropertyAs P2)."
 :body (=>
        (and (Type ?P1 rdf\:Property)
         (PropertyValue daml\:equivalentTo ?P1 ?P2))
        (PropertyValue daml\:samePropertyAs ?P1 ?P2)))


(:name disjointWith-axiom-1
 :description " 'disjointWith' is type 'Property'."
 :body (Type daml\:disjointWith rdf\:Property))


(:name disjointWith-axiom-2
 :description " An object C2 is a value of 'disjointWith' for an object C1 if and only if C1 is type 'Class', C2 is type 'Class', and no object X is both type C1 and type C2."
 :body (<=> (PropertyValue daml\:disjointWith ?c1 ?c2)
        (and (Type ?c1 rdfs\:Class) (Type ?c2 rdfs\:Class)
         (not (exists (?x) (and (Type ?x ?c1) (Type ?x ?c2)))))))


(:name unionOf-axiom-1
 :description " If an object L is a value of 'unionOf' for an object C1, then C1 is type 'Class', L is type 'List', every item in list L is type 'Class', and the objects of type C1 are exactly the objects that are of type one or more of the classes in the list L."
 :body (=> (PropertyValue daml\:unionOf ?c1 ?l)
        (and (Type ?c1 rdfs\:Class) (Type ?l daml\:List)
         (forall (?x)
          (=> (PropertyValue daml\:item ?x ?l) (Type ?x rdfs\:Class)))
         (forall (?x)
          (<=> (Type ?x ?c1)
           (exists (?c2)
            (and (PropertyValue daml\:item ?c2 ?l) (Type ?x ?c2))))))))


(:name disjointUnionOf-axiom-1
 :description " An object L is a value of 'disjointUnionOf' for an object C if and only if L is a value of 'unionOf' for C and L is 'DisjointAll'.  (I.e., an object C is a disjoint union of an object L if and only if L is a list of pairwise disjoint classes and C is the union of the list L of classes.)"
 :body (<=> (PropertyValue daml\:disjointUnionOf ?c ?l)
        (and (PropertyValue daml\:unionOf ?c ?l) (DisjointAll ?l))))


(:name intersectionOf-axiom-1
 :description " An object L is a value of 'intersectionOf' for an object C1 if and only if C1 is type 'Class', L is type 'List', all of the items in list L are type 'Class', and the objects that are type C1 are exactly those objects that are type all of the classes in list L."
 :body (<=> (PropertyValue daml\:intersectionOf ?c1 ?l)
        (and (Type ?c1 rdfs\:Class) (Type ?l daml\:List)
         (forall (?c)
          (=> (PropertyValue daml\:item ?l ?c) (Type ?c rdfs\:Class)))
         (forall (?x)
          (<=> (Type ?x ?c1)
           (forall (?c2)
            (=> (PropertyValue daml\:item ?l ?c2) (Type ?x ?c2))))))))


(:name complementOf-axiom-1
 :description " An object C2 is a value of 'complementOf' for an object C1 if and only if C1 and C2 are disjoint classes and all objects are either type C1 or type C2."
 :body (<=> (PropertyValue daml\:complementOf ?c1 ?c2)
        (and (PropertyValue daml\:disjointWith ?c1 ?c2)
         (forall (?x) (or (Type ?x ?c1) (Type ?x ?c2))))))


(:name oneOf-axiom-1
 :description " An object L is a value of 'oneOf' for an object C if and only if C is type 'Class', L is type 'List', and the objects that are type C are exactly the objects that are values of 'item' for L.  (I.e., saying that C is 'oneOf' L is saying that C is a class, L is a list, and the objects of type C are the objects on the list L.)"
 :body (<=> (PropertyValue daml\:oneOf ?c ?l)
        (and (Type ?c rdfs\:Class) (Type ?l daml\:List)
         (forall (?x)
          (<=> (Type ?x ?c) (PropertyValue daml\:item ?l ?x))))))


(:name onProperty-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'onProperty'.  (I.e., the first argument of onProperty is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:onProperty daml\:Restriction))


(:name onProperty-axiom-2
 :description " 'Property' is the value of 'range' for 'onProperty'.  (I.e., the second argument of onProperty is a property.)"
 :body (PropertyValue rdfs\:range daml\:onProperty rdf\:Property))


(:name toClass-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'toClass'.  (I.e., the first argument of toClass is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:toClass daml\:Restriction))


(:name toClass-axiom-2
 :description " 'Class' is the value of 'range' for 'toClass'.  (I.e., the second argument of toClass is a class.)"
 :body (PropertyValue rdfs\:range daml\:toClass rdfs\:Class))


(:name toClass-axiom-3
 :description " If a property P is a value of 'onProperty' for a restriction R and a class C is a value of 'toClass' for R, then an object I is type R if and only if every value of P for I is type C.  (I.e., a 'toClass' restriction of C on a property P is the class of all objects I such that all values of P for I are type C.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:toClass ?r ?c))
        (forall (?i)
         (<=> (Type ?i ?r)
          (forall (?j) (=> (PropertyValue ?p ?i ?j) (Type ?j ?c)))))))


(:name hasValue-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'hasValue'.  (I.e., the first argument of hasValue is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:hasValue daml\:Restriction))


(:name hasValue-axiom-2
 :description " If a property P is a value of 'onProperty' for a restriction R and an object V is a value for 'hasValue' for R, then an object I is type R if and only if V is a value of P for I.  (I.e., a 'hasValue' restriction of V on a property P is the class of all objects that have V as a value  of P.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:hasValue ?r ?v))
        (forall (?i) (<=> (Type ?i ?r) (PropertyValue ?p ?i ?v)))))


(:name hasClass-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'hasClass'.  (I.e., the first argument of hasClass is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:hasClass daml\:Restriction))


(:name hasClass-axiom-2
 :description " 'Class' is the value of 'range' for 'hasClass'.  (I.e., the second argument of hasClass is a class.)"
 :body (PropertyValue rdfs\:range daml\:hasClass rdfs\:Class))


(:name hasClass-axiom-3
 :description " If a property P is a value of 'onProperty' and a class C is a value of 'hasClass' for a restriction R, then R is a value of 'Type' for an object X if and only if there exists a V that is a value of P for X and that has C as a value of 'Type'.  (I.e., a 'hasClass' restriction of C on a property P is the class of all objects that have a value of P that is type C.)"
 :body (=>
        (and (PropertyValue daml\:hasClass ?r ?c)
         (PropertyValue daml\:onProperty ?r ?p))
        (forall (?x)
         (<=> (Type ?x ?r)
          (exists (?v) (and (PropertyValue ?p ?x ?v) (Type ?v ?c)))))))


(:name minCardinality-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'minCardinality'.  (I.e., the first argument of minCardinality is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:minCardinality
        daml\:Restriction))


(:name minCardinality-axiom-2
 :description " 'NonNegativeInteger' is the value of 'range' for 'minCardinality'.  (I.e., the second argument of minCardinality is a non-negative integer.)"
 :body (PropertyValue rdfs\:range daml\:minCardinality
        rdfs\:NonNegativeInteger))


(:name minCardinality-axiom-3
 :description " If a property P is a value of 'onProperty' for a restriction R and a non-negative integer N is a value of 'minCardinality' for R, then an object I is type R if and only if there is a 'NoRepeatsList' all of whose items are values of P for I and whose length is greater than or equal to N.  (I.e., a 'minCardinality' restriction of N on a property P is the class of all objects I which have at least N values of P.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:minCardinality ?r ?n))
        (forall (?i)
         (<=> (Type ?i ?r)
          (exists (?vl)
           (and (NoRepeatsList ?vl)
            (forall (?v)
             (=> (PropertyValue daml\:item ?vl ?v)
              (PropertyValue ?p ?i ?v)))
            (>= (length ?vl) ?n)))))))


(:name maxCardinality-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'maxCardinality'.  (I.e., the first argument of maxCardinality is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:maxCardinality
        daml\:Restriction))


(:name maxCardinality-axiom-2
 :description " 'NonNegativeInteger' is the value of 'range' for 'maxCardinality'.  (I.e., the second argument of maxCardinality is a non-negative integer.)"
 :body (PropertyValue rdfs\:range daml\:maxCardinality
        rdfs\:NonNegativeInteger))


(:name maxCardinality-axiom-3
 :description " If a property P is a value of 'onProperty' for a restriction R and a non-negative integer N is a value of 'maxCardinality' for R, then an object I is type R if and only if all 'NoRepeatsLists' whose items are exactly the values of P have length less than or equal to N.  (I.e., a 'maxCardinality' restriction of N on a property P is the class of all objects I which have at most N values of P.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:maxCardinality ?r ?n))
        (forall (?i)
         (<=> (Type ?i ?r)
          (forall (?vl)
           (=>
            (and (NoRepeatsList ?vl)
             (forall (?v)
              (<=> (PropertyValue daml\:item ?vl ?v)
               (PropertyValue ?p ?i ?v))))
            (=< (length ?vl) ?n)))))))


(:name cardinality-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'cardinality'.  (I.e., the first argument of cardinality is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:cardinality daml\:Restriction))


(:name cardinality-axiom-2
 :description " 'NonNegativeInteger' is the value of 'range' for 'cardinality'.  (I.e., the second argument of cardinality is a non-negative integer.)"
 :body (PropertyValue rdfs\:range daml\:cardinality
        rdfs\:NonNegativeInteger))


(:name cardinality-axiom-3
 :description " If a property P is a value of 'onProperty' for a restriction R and a non-negative integer N is a value of 'cardinality' for R, then an object I is type R if and only if all 'NoRepeatsLists' whose items are exactly the values of P have length N.  (I.e., a 'cardinality' restriction of N on a property P is the class of all objects I which have exactly N values of P.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:cardinality ?r ?n))
        (forall (?i)
         (<=> (Type ?i ?r)
          (forall (?vl)
           (=>
            (and (NoRepeatsList ?vl)
             (forall (?v)
              (<=> (PropertyValue daml\:item ?vl ?v)
               (PropertyValue ?p ?i ?v))))
            (= (length ?vl) ?n)))))))


(:name hasClassQ-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'hasClassQ'.  (I.e., the first argument of hasClassQ is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:hasClassQ daml\:Restriction))


(:name hasClassQ-axiom-2
 :description " 'Class' is the value of 'range' for 'hasClassQ'.  (I.e., the second argument of hasClassQ is a class.)"
 :body (PropertyValue rdfs\:range daml\:hasClassQ rdfs\:Class))


(:name minCardinalityQ-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'minCardinalityQ'.  (I.e., the first argument of minCardinalityQ is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:minCardinalityQ
        daml\:Restriction))


(:name minCardinalityQ-axiom-2
 :description " 'NonNegativeInteger' is the value of 'range' for 'minCardinalityQ'.  (I.e., the second argument of minCardinalityQ is a non-negative integer.)"
 :body (PropertyValue rdfs\:range daml\:minCardinalityQ
        rdfs\:NonNegativeInteger))


(:name minCardinalityQ-axiom-3
 :description " If a property P is a value of 'onProperty' for a restriction R, a non-negative integer N is a value of 'minCardinalityQ' for R, and a class C is a value of 'hasClassQ' for R, then an object I is type R if and only if there is a 'NoRepeatsList' all of whose items are type C and values of P for I and whose length is greater than or equal to N.  (I.e., a 'minCardinalityQ' restriction of N on a property P is the class of all objects I which have at least N values of P that are type C.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:minCardinalityQ ?r ?n)
         (PropertyValue daml\:hasClassQ ?r ?c))
        (forall (?i)
         (<=> (Type ?i ?r)
          (exists (?vl)
           (and (NoRepeatsList ?vl)
            (forall (?v)
             (=> (PropertyValue daml\:item ?vl ?v)
              (and (PropertyValue ?p ?i ?v) (Type ?v ?c))))
            (>= (length ?vl) ?n)))))))


(:name maxCardinalityQ-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'maxCardinalityQ'.  (I.e., the first argument of maxCardinalityQ is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:maxCardinalityQ
        daml\:Restriction))


(:name maxCardinalityQ-axiom-2
 :description " 'NonNegativeInteger' is the value of 'range' for 'maxCardinalityQ'.  (I.e., the second argument of maxCardinalityQ is a non-negative integer.)"
 :body (PropertyValue rdfs\:range daml\:maxCardinalityQ
        rdfs\:NonNegativeInteger))


(:name maxCardinalityQ-axiom-3
 :description " If a property P is a value of 'onProperty' for a restriction R, a non-negative integer N is a value of 'maxCardinalityQ' for R, and a class C is a value of 'hasClassQ' for R, then an object I is type R if and only if all 'NoRepeatsLists' whose items are exactly the values of P that are type C have length less than or equal to N.  (I.e., a 'maxCardinalityQ' restriction of N on a property P is the class of all objects I which have at most N values of P that are type C.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:maxCardinalityQ ?r ?n)
         (PropertyValue daml\:hasClassQ ?r ?c))
        (forall (?i)
         (<=> (Type ?i ?r)
          (forall (?vl)
           (=>
            (and (NoRepeatsList ?vl)
             (forall (?v)
              (<=> (PropertyValue daml\:item ?vl ?v)
               (and (PropertyValue ?p ?i ?v) (Type ?v ?c)))))
            (=< (length ?vl) ?n)))))))


(:name cardinalityQ-axiom-1
 :description " 'Restriction' is a value of 'domain' for 'cardinalityQ'.  (I.e., the first argument of cardinalityQ is a restriction.)"
 :body (PropertyValue rdfs\:domain daml\:cardinalityQ
        daml\:Restriction))


(:name cardinalityQ-axiom-2
 :description " 'NonNegativeInteger' is the value of 'range' for 'cardinalityQ'.  (I.e., the second argument of cardinalityQ is a non-negative integer.)"
 :body (PropertyValue rdfs\:range daml\:cardinalityQ
        rdfs\:NonNegativeInteger))


(:name cardinalityQ-axiom-4
 :description " If a property P is a value of 'onProperty' for a restriction R, a non-negative integer N is a value of 'cardinalityQ' for R and a class C is a value of 'hasClassQ' for R, then an object I is type R if and only if all 'NoRepeatsLists' whose items are exactly the values of P that are type C have length N.  (I.e., a 'cardinalityQ' restriction of N on a property P is the class of all objects I which have exactly N values of P that are type C.)"
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:cardinalityQ ?r ?n)
         (PropertyValue daml\:hasClassQ ?r ?c))
        (forall (?i)
         (<=> (Type ?i ?r)
          (forall (?vl)
           (=>
            (and (NoRepeatsList ?vl)
             (forall (?v)
              (<=> (PropertyValue daml\:item ?vl ?v)
               (and (PropertyValue ?p ?i ?v) (Type ?v ?c)))))
            (= (length ?vl) ?n)))))))


(:name inverseOf-axiom-1
 :description " 'inverseOf' is type 'Property'."
 :body (Type daml\:inverseOf rdf\:Property))


(:name inverseOf-axiom-2
 :description " An object P2 is a value of 'inverseOf' for an object P1 if and only if P1 is type 'AbstractProperty', P2 is type 'AbstractProperty', and an object X2 is a value of P1 for an object X1 if and only X1 is a value of P2 for X2."
 :body (<=> (PropertyValue daml\:inverseOf ?p1 ?p2)
        (and (Type ?p1 daml\:AbstractProperty)
         (Type ?p2 daml\:AbstractProperty)
         (forall (?x1 ?x2)
          (<=> (PropertyValue ?p1 ?x1 ?x2)
           (PropertyValue ?p2 ?x2 ?x1))))))


(:name first-axiom-1
 :description " 'first' is type 'UniqueProperty'."
 :body (Type daml\:first daml\:UniqueProperty))


(:name first-axiom-2
 :description " An object X is the value of 'first' for an object L if and only if L is type 'List' and the value of '_1' for L is X.  (I.e., 'first' is '_1' for lists.)"
 :body (<=> (PropertyValue daml\:first ?l ?x)
        (and (Type ?l daml\:List) (PropertyValue rdf\:_1 ?l ?x))))


(:name rest-axiom-1
 :description " 'rest' is type 'UniqueProperty'."
 :body (Type daml\:rest daml\:UniqueProperty))


(:name rest-axiom-2
 :description " An object R is the value of 'rest' for an object L if and only if L is type 'List', R is type 'List', and L has the same items in the same order as list R with one additional object as its first item."
 :body (<=> (PropertyValue daml\:rest ?l ?r)
        (and (Type ?l daml\:List) (Type ?r daml\:List)
         (exists (?x) (= ?l (cons ?x ?r))))))


(:name item-axiom-1
 :description " 'item' is type 'Property'."
 :body (Type daml\:item rdf\:Property))


(:name item-axiom-2
 :description " An object X is a value of 'item' for an object L if and only if L is type 'List' and either X is the value of 'first' for L or X is a value of 'item' for the value of 'rest' of L.  (I.e., Saying that X is an item of L is saying that X is the first item in list L or there is a list R that is the rest of list L and X is an item in the list R.)"
 :body (<=> (PropertyValue daml\:item ?l ?x)
        (and (Type ?l daml\:List)
         (or (PropertyValue daml\:first ?l ?x)
          (exists (?r)
           (and (PropertyValue daml\:rest ?l ?r)
            (PropertyValue daml\:item ?r ?x)))))))


(:name versionInfo-axiom-1
 :description " 'versionInfo' is a property."
 :body (Type daml\:versionInfo rdf\:Property))


(:name imports-axiom-1
 :description " 'imports' is a property."
 :body (Type daml\:imports rdf\:Property))


(:name nil-axiom-1
 :description " 'nil' is a list for which there are no values of 'item'.  (I.e., 'nil' is the empty list.)"
 :body (Type daml\:nil daml\:List))


(:name nil-axiom-2
 :description " 'nil' is a list for which there are no values of 'item'.  (I.e., 'nil' is the empty list.)"
 :body (not (PropertyValue daml\:item daml\:nil ?x)))