Generation of minimal models

[ignazio1977]

On Tue, Oct 15, 2013 at 12:34 PM, Ignazio Palmisano [email protected] wrote:
On 15 October 2013 20:22, Chris Mungall [email protected] wrote:

Given an ontology, and a class C, if C is satisfiable, can we materialize
the minimal interpretation / ABox of the ontology? E.g. given the pizza
ontology, if cheesy pizza is satisfiable, then we know that there exists
some meat pizza, i.e. we know the following abox is entailed

_x Type MeatPizza
_y Type MeatTopping
_x hasTopping _y

This seems like a useful operation. E.g. for a pizza application that allows
us to generate a "prototypical" pizza instance (replacing anon individuals
with UUIDs) and then customize it. Or perhaps someone describing an
anatomical abnormality could generate a minimal model from a canonical
anatomical ontology and then modify it.

That sounds like an interesting feature. I'm not sure of the
implications yet - I suppose that implementing it inside a reasoner
would be easier.

About 'minimal', that rings a few alarm bells - I have the feeling it
might be really hard to ensure minimality, although I don't have
references to flesh out the feeling.

Yes, my intuition originally was that profiles that exclude constructs like disjunction would make this easier

I think it's also useful for ontology editors - sometimes the minimal
interpretation may differ from what the author thinks it is. Visualizing the
minimal model given a satisfiable class can help illustrate this.

Yes, I was thinking of Matthew Horridge's explanations; I think this
would be very useful as a companion tool.
https://www.escholar.manchester.ac.uk/uk-ac-man-scw:131699

Perhaps - but certainly not as well thought out at this stage!

Is the term "minimal model" correct here? I've seen this used in the logic
programming literature, I'm not aware of a definitive definition, but
perhaps this is obvious to logic gurus.

I'm waiting for them to weigh in :-)

If we restrict ourselves to EL++, is the calculation of the minimal model
trivial? - and is there OWLAPI code for doing this? Maybe something that
falls out of an existing reasoner implementation.

FaCT++ has code to expose some of the tableaux model through the
OWLKnowledgeExplorerReasoner interface. I don't know whether this is
useful or sufficient for this task.
There is no code in the OWLAPI for this at the moment, but it strikes
me as an interesting tool that would fit nicely in OWLAPITOOLS. If you
don't mind I'm going to lift this conversation and use it as a feature
request.

Absolutely, go ahead. At this stage I'm not sure how important this will turn out to be,
but if it sounds interesting go for it.

I actually have some code at the moment that does something similar, although
it is slightly different, as for various reasons it makes assumptions that are not
guaranteed to be valid, but are a useful heuristic (i.e. it's a hack). For example, that certain classes
are only instantiated once. Ideally this would be a separate heuristic layer on top of a
guaranteed valid implementation. It also attempts to partially support inverses whilst
using Elk, in a limited way.

I.

I have a feeling there is a chunk of the DL literature I'm unaware of that
explores this in more depth.

There is stuff on finite versus infinite domains, and that's a very
rough separation that would be useful here - if the domain is
infinite, there is no way to create a small abox that represents it
all :-P but I'm not enough of a DL guru to say more than that.
I.