(iff (type ?x ?y) (?y ?x))
(implies (?x ?y)(class ?x))
(implies (?x ?y ?z)(relation ?x))
(iff (subclass ?x ?y)(forall (?z)(implies (?x ?z)(?y ?z))))
(implies (and (domainof ?x ?y)(?x ?u ?v))(?y ?u))
(implies (and (rangeof ?x ?y)(?x ?u ?v))(?y ?v))
(T ?x)
(not (F ?x))
(iff (symmetric ?x)(iff (?x ?y ?z))(?x ?z ?y)))
(implies (restriction ?x)(class ?x))
(iff (inverse ?x ?y)(iff (?x ?u ?v)(?y ?v ?u)))
(iff (functnl ?x)(forall (?u ?v ?w)(implies (and (?x ?u ?v)(?x ?u ?w))(= ?v ?w)))))
(iff (ifunctnl ?x)(forall (?u ?v ?w)(implies (and (?x ?v ?u)(?x ?w ?u))(= ?v ?w)))))
(iff (transitive ?x)(forall (?u ?v ?w)(implies (and (?x ?u ?v)(?x ?v ?w))(?x ?u ?w))))

 

a rdf:type b (type a b)
rdf:Class class
a rfds:subClassOf b (subclass a b)
a rdfs:domain b (domainof a b)
a rdfs:range b (rangeof a b)
owl:Thing T
owl:Nothing F
owl:Class class
owl:SymmetricProperty symmetric
owl:FunctionalProperty functnl
owl:InverseFunctionalProperty ifunctnl
owl:TransitiveProperty transitive
a owl:onProperty b irp(a) = b
a owl:sameIndividualAs b (= a b)
a owl:differentIndividualFrom b (not (= a b))
a owl:DisjointWith b (not (and (a ?x)(b ?x)))
a owl:complementOf b (iff (a ?x)(not (b ?x)))
a owl:inverseOf b (inverse a b)
a owl:oneOf b1 ...bn (or (= a b1)(= a b2)....(= a bn))
a owl:unionOf b1 ... bn (iff (a ?x)(or (b1 ?x) .... (bn ?x)))
a owl:intersectionOf b1 ... bn (iff (a ?x)(and (b1 ?x) .... (bn ?x)))
a owl:allValuesFrom b

(iff (a ?x)
(forall (?y)(implies ((irp a) ?x ?y)(b ?y)))
)
a owl:someValuesFrom b (iff (a ?x)
(exists (?y)(and ((irp a) ?x ?y)(b ?y)))
)
a owl:hasValue b (iff (a ?x) ((irp a) ?x b))
a owl:minCardinality n (iff (a ?x)
(exists (?x1 ... ?xn)
(and (not (= ?x1 ?x2))....(not (= ?xn-1 ?xn))
((irp a) ?x ?x1)....((irp a) ?x ?xn) )))
a owl:maxCardinality n (iff (a ?x)
(not
(exists (?x1 ... ?xn+1)
(and (not (= ?x1 ?x2))....(not (= ?xn ?xn+1))
((irp a) ?x ?x1)....((irp a) ?x ?xn+1) ))))
a owl:cardinality n (iff (a ?x)
(and
(exists (?x1 ... ?xn)
(and (not (= ?x1 ?x2))....(not (= ?xn-1 ?xn))
((irp a) ?x ?x1)....((irp a) ?x ?xn) )))
(not
(exists (?x1 ... ?xn+1)
(and (not (= ?x1 ?x2))....(not (= ?xn ?xn+1))
((irp a) ?x ?x1)....((irp a) ?x ?xn+1) )))))