// namespace abbreviations
//ex := 'http://www.example.org/ex#'.
rdf := 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'.
rdfs := 'http://www.w3.org/2000/01/rdf-schema#'.
owl := 'http://www.w3.org/2002/07/owl#'.

FORALL Mdl @owl_lite_(Mdl) {
  // copy all facts from Mdl to current model
  FORALL X,Y,Z X[Y->Z] <- X[Y->Z]@Mdl.

  // ------------- rdfs class axioms -------------------------

  // rdfs:subClassOf
  FORALL O,V      O[rdfs:subClassOf->V] <-
      EXISTS W   (O[rdfs:subClassOf->W] AND W[rdfs:subClassOf->V]).
  FORALL O,T      O[rdf:type->T] <-
      EXISTS S   (S[rdfs:subClassOf->T] AND O[rdf:type->S]).

  // ------------- rdfs property axioms ----------------------

  // rdfs:subPropertyOf
  FORALL O,V      O[rdfs:subPropertyOf->V] <-
      EXISTS W   (O[rdfs:subPropertyOf->W] AND W[rdfs:subPropertyOf->V]).
  FORALL O,P,V    O[P->V] <-
      EXISTS S   (S[rdfs:subPropertyOf->P] AND O[S->V]).

  // rdfs:domain DL-style
  FORALL O,T      O[rdf:type->T] <-
      EXISTS P,V (O[P->V] AND P[rdfs:domain->T]).
  // rdfs:range DL-style
  FORALL V,T      V[rdf:type->T] <-
      EXISTS O,P (O[P->V] AND P[rdfs:range->T]).

  // ------------- owl property axioms -----------------

  // owl:ObjectProperty has range and domain owl:Class
  owl:ObjectProperty[rdfs:domain->owl:Class].
  owl:ObjectProperty[rdfs:range->owl:Class].

  // owl:inverseOf
  owl:inverseOf[rdfs:domain->owl:ObjectProperty].
  owl:inverseOf[rdfs:range->owl:ObjectProperty].
  owl:inverseOf[rdf:type->owl:SymmetricProperty].
  FORALL O,P,V    V[P->O] <-
      EXISTS Q   (O[Q->V] AND P[owl:inverseOf->Q]).

  // owl:TransitiveProperty
  FORALL O,P,V    O[P->V] <- 
      EXISTS W   (O[P->W] AND W[P->V]) AND P[rdf:type->owl:TransitiveProperty].

  // owl:SymmetricProperty
  FORALL O,P,V    V[P->O] <-
                  O[P->V] AND P[rdf:type->owl:SymmetricProperty].

  FORALL P,V      P[rdfs:domain->V] <-
                  P[rdf:type->owl:SymmetricProperty]
              AND P[rdfs:range->V].

  FORALL P,V      P[rdfs:range->V] <-
                  P[rdf:type->owl:SymmetricProperty]
              AND P[rdfs:domain->V].

  // ------------- (in)equality -----------------  

  // reflexiveProperty
  FORALL O,P,V    O[P->V] <-
                  O[P->V]
              AND P[rdf:type->reflexiveProperty].

  // owl:equivalentProperty
  owl:equivalentProperty[rdf:type->owl:SymmetricProperty].
  owl:equivalentProperty[rdf:type->owl:TransitiveProperty].
  owl:equivalentProperty[rdf:type->reflexiveProperty].
  FORALL O,P,Q,V  O[Q->V] <-
     EXISTS Q    (P[owl:equivalentProperty->Q] AND O[P->V]).
  FORALL N,O,P,V  N[P->V] <-
                  N[owl:equivalentProperty->O] AND O[P->V].
  FORALL O,P,V,W  O[P->W] <-
                  V[owl:equivalentProperty->W] AND O[P->V].

  // owl:equivalentClass
  owl:equivalentClass[rdf:type->owl:SymmetricProperty].
  owl:equivalentClass[rdf:type->owl:TransitiveProperty].
  owl:equivalentClass[rdf:type->reflexiveProperty].
  FORALL O,T      O[rdf:type->T] <-
      EXISTS S   (T[owl:equivalentClass->S] AND O[rdf:type->S]).
  FORALL O,P,Q,V  O[Q->V] <-
                  P[owl:equivalentClass->Q] AND O[P->V].
  FORALL N,O,P,V  N[P->V] <-
                  N[owl:equivalentClass->O] AND O[P->V].
  FORALL O,P,V,W  O[P->W] <-
                  V[owl:equivalentClass->W] AND O[P->V].

  // ----------------- property restrictions --------

  // owl:onProperty, owl:allValuesFrom
  FORALL O,R,P    O[rdf:type->R] <-
      EXISTS V    O[P->V]
              AND R[rdf:type->owl:Restriction]
              AND R[owl:onProperty->P]
              AND EXISTS C R[owl:allValuesFrom->C].
}