(: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 rdf:type ?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 NoRepeatsTuple-axiom-1
:description " Item is a binary relation that relates a tuple to its elements. X is
an item of tuple T if and only if T is not the EmptyTuple and either X
is the first of T or X is an item of the rest of T.
"
:body (not (Item ?t EmptyTuple)))
(:name NoRepeatsTuple-axiom-2
:description " Item is a binary relation that relates a tuple to its elements. X is
an item of tuple T if and only if T is not the EmptyTuple and either X
is the first of T or X is an item of the rest of T.
"
:body (<=> (Item ?t (Cons ?x ?r)) (or (= ?t ?x) (Item ?t ?r))))
(:name NoRepeatsTuple-axiom-3
:description " The length of a tuple is the number of elements in the tuple. L is
the length of tuple T if and only if either T is the empty tuple and L
is 0 or L is 1 plust the length of the rest of T.
"
:body (<=> (= (Length ?t) 0) (= ?t EmptyTuple)))
(:name NoRepeatsTuple-axiom-4
:description " The length of a tuple is the number of elements in the tuple. L is
the length of tuple T if and only if either T is the empty tuple and L
is 0 or L is 1 plust the length of the rest of T.
"
:body (= (Length (Cons ?x ?t)) (+ 1 (Length ?t))))
(:name NoRepeatsTuple-axiom-5
:description " A NoRepeatsTuple is a tuple for which no item occurs more than once.
T is a NoRepeatsTuple if and only if T is EmptyTuple, EmptyTuple is the
rest of T, or the first of T is not an item of the rest of T and the
rest of T is a NoRepeatsTuple.
"
:body (<=> (NoRepeatsTuple ?t) (or (= ?t EmptyTuple) (= (Rest ?t) EmptyTuple) (and (not (Item (First ?t) (Rest ?t)) (NoRepeatsTuple (Rest ?t)))))))
(: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\".
"
: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.
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.
"
:body (PropertyValue rdfs:domain rdfs:seeAlso rdfs:Resource))
(:name seeAlso-axiom-2
:description " \"Resource\" is a value of both \"domain\" and \"range\" for \"seeAlso.
"
: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\".
"
: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 " \"AbstractProperty\" is a subclass of \"Property\".
"
:body (PropertyValue subClassOf daml:AbstractProperty rdf:Property))
(:name DatatypeProperty-axiom-1
:description " \"DatatypeProperty\" is a subclass of \"Class\".
"
:body (PropertyValue subClassOf daml:DatatypeProperty rdf:Property))
(: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\".
"
: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\".
"
: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\".
"
: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 \"NoRepeatsTuple\" 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 (NoRepeatsTuple ?vl) (forall (?v) (=> (Item ?vl ?v) (PropertyValue ?p ?i ?v))) (Length ?v1 ?l) (>= ?l ?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\".
"
: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 \"NoRepeatsTuples\" 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 (NoRepeatsTuple ?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\".
"
: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 \"NoRepeatsTuples\" 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 (NoRepeatsTuple ?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\".
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 \"NoRepeatsTuple\" all of whose items are type C
and values of P for I and whose length is greater than or equal to N.
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 (NoRepeatsTuple ?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\".
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 \"NoRepeatsTuples\" 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 (NoRepeatsTuple ?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\".
"
: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 \"NoRepeatsTuples\" 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 (NoRepeatsTuple ?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)))