A use for 2 model theories?? was: Re: revised version of semantics document

Jos De_Roo wrote:
>
>
> OK, fine
> if you don't like that, you just write
>
> ==== peterP1
> @prefix : <university#> .
>
> :John a :Student .
> :John a :Employee .
> ====
>
> and jon's agents somewhere came accross
> (remark the unnamed class _:U)
>
> ==== jonP1
> @prefix owl: <http://www.w3.org/2002/07/owl#> .
> @prefix : <university#> .
>
> _:U owl:intersectionOf ( :Student :Employee ) .
> ====
>
> then you could still OWL-entail
>
> ==== peterC1
> @prefix owl: <http://www.w3.org/2002/07/owl#> .
> @prefix : <university#> .
>
> :John a _:X .
> _:X owl:intersectionOf ( :Student :Employee ) .
> ====
>
> but you would indeed need jonP1
> it matters because of
> all models of the premis are also models of the conclusion
> and no new existentials are introduced in the entailment rules
>

Aha, so if there was some process that could generate the hypothetical
classes for me, e.g.

_:U owl:intersectionOf(:Student, :Employee) .

then a GHOWL reasoner could 'deduce' the desired relationships. That is to
say, these classes would be 'interesting' only if they had, perhaps, a
non-zero number of instances.

This still raises the question of where these classes might come from.
Perhaps a reasoner implemented according to Peter's MT, might generate them
in the first place? Perhaps there is a role for _both_ forms of the MT:
using your device, we might obtain the necessary entailments for GHOWL.

The question which this now raises in my mind is: given this device, is
there a difference in the entailments licensed by either Peter's or Pat's
MT? If not, what are the functional differences?

Jonathan