Reasoner does not check cardinalities and/or restrictions?

I tried to create the perhaps simplest ontology, consisting of two classes (A, B) and a relation (R) between the two classes. I also want to state that every individual of A must have a relation R with some other individual.

:R rdf:type owl:ObjectProperty ;
   rdfs:domain :A ;
   rdfs:range :B .

:A rdf:type owl:Class ;
   rdfs:subClassOf owl:Thing ,
                   [ rdf:type owl:Restriction ;
                     owl:onProperty :R ;
                     owl:someValuesFrom :B
                   ] ;
   owl:disjointWith :B .

:B rdf:type owl:Class ;
   rdfs:subClassOf owl:Thing .

Now some individuals:

:a1 rdf:type :A , owl:NamedIndividual ; :R :b1 .
:a2 rdf:type :A , owl:NamedIndividual .
:b1 rdf:type :B , owl:NamedIndividual .

enter image description here

But the reasoner does not complain about a2 not having a relation R. Why?

(Note: I created ontology in Protégé; I tried FacT++ and HermiT reasoners)

Solution

I also want to state that every individual of A must have a relation R with some other individual.

You have done this correctly. When you go on to assert that

:a1 rdf:type :A , owl:NamedIndividual ; :R :b1 .
:a2 rdf:type :A , owl:NamedIndividual .
:b1 rdf:type :B , owl:NamedIndividual .

the reasoner will correctly infer there is some value, let's call it X, such that :a2 :R X and that X rdf:type :B. OWL reasoning uses the open world assumption. This means that if something is not explicitly stated to be true or false, it is not assumed to be false or true, but rather unknown. E.g., you could correctly assert that

Human ⊑ ∃ hasMother.Human

that is, that every Human has some Human as a mother. If I say that

DanielWebster ∈ Human

and that's all that I say; I haven't made an inconsistency. There are just things that are true that we don't know yet. We know that DanielWebster has a mother, but we don't know who she is.

If you want to close the world, you could do a few things, but the results may not be what you want. First, you could make B an enumerated class. That is, you could explicitly list the individuals of B:

B ≡ {b1}

That actually won't lead to an inconsistency, though. In fact, the reasoner will infer that since a2 must be related to some B, and the only B is b1, that a2 is related by R to b1.