From what I've understood as reading the book Foundations of Semantic Web Technologies concerning owl formal semantics, Hitzler et al have put forward two kinds of model-theoretic semantics for SROIQ: one is the model checking like approach (where we check different interpretations to find the models of our KB) and the other is via predicate logic. In the latter approach, the book just translates SROIQ into predicate logic.
However, the book is a bit confusing for me and I do not know if I have gotten some points right, so here are my questions:
Is model-checking a kind of model-theoretic semantics?
Is translating your SROIQ into predicate logic also a model-theoretic semantics?
How is translating SROIQ into predicate logic a kind of "semantics"? Is that because after the conversion, we can pick up FOL semantics and algorithms?
Thanks!
P.S. This is a link to the book! Just in case!
Model theoretic semantics is how you determine the meaning of axioms - i.e., what rules are available to build a model or to check it is a valid one. Two examples: OWL semantics and RDF semantics. They have a lot of overlap but are not identical.
Model checking does not define semantics, it applies semantic rules defined in a model to actual knowledge bases. Translation to another formalism, e.g., predicates, might maintain the same semantics (i.e., all models stay the same in both formalisms), but this depends on the formalism involved.