What are the rules used by a reasoner

Question

In OWL.

I know that if

ObjectProperty AB

and

AB domain A

and

AB range B

and

A subClassOf AB something

then the reasoner can infer that

A subClassOf B

1- What is the notion behind this inference?

2- Is there any references that explains the whole set of rules for how does the reasoner works, i.e. what are the rules that a reasoner applies to turn implicit knowledge into explicit one? like this one presented in the example above?

Answer 1

The reasoning behind these inferences follows the rules outlined here: http://www.w3.org/TR/owl2-direct-semantics/#Object_Property_Expression_Axioms