Relating to inferred axiom generators

[alanruttenberg]

In a recent release of IAO, http://purl.obolibrary.org/obo/2017-01-06/iao.owl three issues arose related to inferred axiom generation.

The use case is to release a merged, pre-reasoned ontology. To do this I use the inferred axiom generators to add axioms to the stated ontology.

1. When using InferredObjectPropertyCharacteristicAxiomGenerator, axioms may be generated that when added to the original ontology violate the general restrictions. Proposed remediation: Add a method or parameter that disallows this. https://github.com/information-artifact-ontology/IAO/issues/195

2. Once I stopped using the above, I found that including the axioms from InferredSubObjectPropertyAxiomGenerator led to my ontology having unsatisfiable classes. I'm confused about how this could ever happen. Proposed remediation: either help me understand why this could make sense, or fix bug if it doesn't. https://github.com/information-artifact-ontology/IAO/issues/195

3. https://github.com/information-artifact-ontology/IAO/issues/196 notes that axioms that might be considered redundant (because there are already logically equivalent axioms) are added. I'm uncertain as whether and if, how this should be remediated. An example:

ObjectProperty: <http://purl.obolibrary.org/obo/IAO_0000223> InverseOf: inverse(<http://purl.obolibrary.org/obo/IAO_0000223>)

[sesuncedu]

Which property characteristics did you hit? I've seen and fixed one issue with vacuously transitive properties (e.g. if range and domain were disjoint). It's valid, but useless, and murphy says it's going to take you out of DL. I think this was the first patch I ever submitted.

Asymmetric is more reasonable except when forbidden (oh hELl).

I guessed you were using Hermit from the weird inverseness. Not wrong...unless target profile forbids inverse (hELp) .

Not sure why there would be unsatisfiable classes unless there's a bug. I think they would be valid if in profile and not having any asserted instances. I can't think of any reason why you'd want them.

I'm now wondering how hard it would be to use part of the profile checkers to filter out inferred axioms that would take one out of profile. Some are standalone, but things that hit role chains require wider scope.

I also wonder if it is necessary to add inferred axioms to the base ontology and reclassified as processing continues. It might even be necessary to iterate until a fixed point is found. Unfortunately, things like hermits fondness for inverse property expressions make me a bit nervous, since that is a real example of where things could diverge.

There's a related issue with meta-punning; if the reasoner doesn't reject uses of reserved vocabulary, you can end up with subclasses of owl:Class turning into classes (though that requires round-trip through rdf).

I will take a look and see if I can get a handle on what's messed up. Does the generation process require CL? I have an SBCL environment set up , but I would guess at ABCL because Java?

Simon

[alanruttenberg]

Here is a small example for the first issue. partof and occurs-in are both non-simple. Both are inferred to be asymmetric and irreflexive by the generator. However adding them violates the global restrictions and one gets the error Non-simple object property 'http://example.com/contains-process' is used as a simple one

Prefix(:=<urn:lsw:ontology:naughty-inferred#>)
Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)

Ontology(<urn:lsw:ontology:naughty-inferred>

Declaration(Class(:continuant))
Declaration(Class(:occurrent))
Declaration(ObjectProperty(:contains-process))
Declaration(ObjectProperty(:haspart))
Declaration(ObjectProperty(:occurs-in))
Declaration(ObjectProperty(:partof))

InverseObjectProperties(:contains-process :occurs-in)
InverseObjectProperties(:haspart :partof)

ObjectPropertyDomain(:occurs-in :occurrent)
ObjectPropertyRange(:occurs-in :continuant)

TransitiveObjectProperty(:partof)

DisjointClasses(:continuant :occurrent)

SubObjectPropertyOf(ObjectPropertyChain (:occurs-in :partof) :occurs-in)
SubObjectPropertyOf(ObjectPropertyChain (:partof :occurs-in) :occurs-in)
) 

[ignazio1977]

Which reasoner is involved?

[alanruttenberg]

To your other questions/comments:

I'm using full OWL-DL

I used HermiT, but also tested FaCT++

I could use the profile checkers, but it would be ugly and I expect that anyone else hitting this issue isn't going to want those axioms either. Also, one would have to be careful to only throw out the generated axioms.

We add axioms to the base ontology because many people who use them don't run a reasoner. Generating subclass axioms, minimally, helps avoid misunderstanding. It is possible that adding axioms will help with queries on less able sparql engines. But to tell the truth, I didn't do an analysis of which would be useful or not. My model was that all the inferred axioms are correct and there is no disadvantage to include them, but a possible advantage.

I do all my work with ABCL on java because its easy to use the OWLAPI from there. I don't think you need to run my tools for the analysis. Above I gave the merged ontology. You can get the told version at http://purl.obolibrary.org/obo/iao/2017-01-06/iao-stated.owl

Or you can clone https://github.com/information-artifact-ontology/IAO/

releases/2017-01-06/iao.owl is the told version (which imports some ontologies in the same directory) releases/2017-01-06/iao-merged.owl is the same as the one at the URL cited above.

I will see if I can get a smaller example for the second issue, one for which generated subproperty axioms introduce unsatisfiables.

[sesuncedu]

Thanks

Separating out the generated axioms from the told ones is easy, since the generated axioms are going into a fresh ontology.

Profile checking in this situation might be really easy if the inferred axiom is a profile violation in itself (there are Visitors that may be accessible). Inferred property-unsimplifiers could be removed if the properties aren't mentioned in forbidden places. I'm not sure how easy that would be in practice.

Simon

[alanruttenberg]

Arguably the conflicting axioms are not sanctioned entailments. The conformance document defines entailment as between two consistent OWL2 DL Ontology documents. In our case, the ontologies would be the told version and the one augmented by the inferred axioms. However since the latter violates the general restrictions it isn't really an OWL2 DL ontology document, and in any case can't be checked for consistency. https://www.w3.org/TR/owl2-conformance/#Entailment_Checker

When using the Direct Semantics, Ont(d1) and Ont(d2) denote ontology structures that satisfy all of the restrictions on OWL 2 ontologies described in Section 3 of the OWL 2 Syntax specification

[alanruttenberg]

Here's a bit from the explanation generator for a case 2 entailment that shouldn't be the case. I'm still trying to grok it, but maybe you can see something quicker.

[alanruttenberg]

I'm having trouble reproducing the unsatisfiable classes case. Until further notice don't pursue this. Perhaps I confused myself with the various versions and tests I was doing.

[alanruttenberg]

OK, here's something to look at. Not as small, unfortunately. Below are 4 ontologies. The first(1) was generated including InferredObjectPropertyCharacteristicAxiomGenerator and InferredSubObjectPropertyAxiomGenerator. It can't be reasoned over because of introduced violation of general restrictions.

The second was made by editing the first and removing all Irreflexive and Asymmetric property axioms, other than the single one that was in the source. If you reason over it you will find 64 unsatisfiable classes.

The third was made by editing the second and removing EquivalentProperties, SubObjectPropertyOf, and InverseObjectProperties axioms where one of the arguments was an InverseOf() expression. None of these were in the original - they were added by one or another of the generators. There are no unsatisfiable classes in this version.

The fourth is just a list of those axioms that were removed, as a sanity check.

Hopefully this will be enough for you to track down what the issue is.

Along the way to doing this I got the most bizarre behavior. Starting with the first second ontology below, one by one I would remove one of the object property axioms that used InverseOf. Each time I would run the reasoner to check for unsatisfiable classes. After removing some number, mostly from the properties below part of, and has part, all of a sudden I get an error of violating the general restrictions, complaining, effectively, about is member of, which is irreflexive (in the source). ??? Note that the third ontology below, the one that has no unsatisfiable classes, the IrreflexiveObjectProperty axiom is intact.

1. iao-merged.owl.txt
2. iao-merged-without-inferred-object-property-characteristics.owl.txt
3. iao-merged-without-inferred-object-property-characteristics-or-inverse-of-inverse-of.owl.txt
4. only-inverse-of-inverse-of-axioms.owl.txt

[alanruttenberg]

A couple more things:

InferredDataPropertyCharacteristicAxiomGenerator generates functional data property axioms even for properties which already have such an axiom.

InferredEquivalentDataPropertiesAxiomGenerator generates equivalentDataProperties axioms with a single argument - the property, for each data property in the ontology. These axioms are subsequently ignored when serializing an ontology to which they have been added.

As noted earlier, InferredInverseObjectPropertiesAxiomGenerator generates, for each object property OP, an axiom InverseObjectProperties(OP ObjectInverseOf(OP)). It also reiterates already stated InverseObjectProperty axioms.

[ignazio1977]

Great report, thank you.

Equivalent data properties with only one element was a bug in the generator, fixed under #527 (released in OWLAPI 4.2.8) - HermiT (version 1.3.8.413, that is included with Protege) uses an older version and that's the reason for that bug still being seen.

Protege is in the process of moving to OWLAPI 4.3.0, so a few of these should disappear shortly. I'll update the HermiT fork and make another release once I've checked the other problems and ensured they're fixed.

[ignazio1977]

InferredInverseObjectPropertiesAxiomGenerator generates, for each object property OP, an axiom InverseObjectProperties(OP ObjectInverseOf(OP))

This is a fresh bug, will be fixed in the next release.

Duplicate axioms are wasteful but checking if they already exist might have a computationally similar cost (it's necessary to check existence with and without annotations).

[ignazio1977]

Fixed the duplication and most of the non simple violations introduced by inferred axioms.

I've got to the stage where I'm getting unsatisfiable classes; when looking for explanations, I've found the following exception coming up:

Exception in thread "main" java.lang.IllegalArgumentException: Non-simple property '<http://purl.obolibrary.org/obo/RO_0002351>' or its inverse appears in irreflexive object property axiom.
    at org.semanticweb.HermiT.structural.ObjectPropertyInclusionManager.rewriteAxioms(ObjectPropertyInclusionManager.java:108)
    at org.semanticweb.HermiT.structural.OWLClausification.preprocessAndClausify(OWLClausification.java:163)

As the irreflexive axioms are not generated for simple properties, I'm guessing the property is simple /at the time the check is carried out/ - but that's no longer the case at the end of the generation. The axiom generation generates each axiom by testing if it is entailed by the ontology, but it does not take other inferrable axioms into account - one or the other would not be entailed, depending on order.

That sounds non deterministic and nonmonotonic too - I'm probably missing a facet of the problem.

[ignazio1977]

Skipping axioms of the kind

SubObjectPropertyOf(<http://purl.obolibrary.org/obo/OBI_0000299> ObjectInverseOf(<http://purl.obolibrary.org/obo/RO_0000056>))

makes the problem go away. However I'm not clear on why. When asked for getSuperObjectProperties() the reasoner responds with object property expressions that include inverse expressions, and the axiom is entailed.

[ignazio1977]

From https://www.w3.org/TR/owl2-syntax/#Property_Hierarchy_and_Simple_Object_Property_Expressions

An object property expression OPE is composite in the set of axioms Ax if

OPE is equal to owl:topObjectProperty or owl:bottomObjectProperty, or Ax contains an axiom of the form SubObjectPropertyOf( ObjectPropertyChain( OPE1 ... OPEn ) OPE ) with n > 1, or SubObjectPropertyOf( ObjectPropertyChain( OPE1 ... OPEn ) INV(OPE) ) with n > 1, or TransitiveObjectProperty( OPE ), or TransitiveObjectProperty( INV(OPE) ).

Among the explanations for inconsistent classes, I have the following:

Asserted by inference generators:

EquivalentObjectProperties(<RO_0002351> ObjectInverseOf(<RO_0002350>) )
SubObjectPropertyOf(<RO_0002351> ObjectInverseOf(<BFO_0000050>))
IrreflexiveObjectProperty(<RO_0002350>)

explanation for

[TransitiveObjectProperty(<BFO_0000050>),
 SubObjectPropertyOf(<RO_0002351> ObjectInverseOf(<BFO_0000050>)),
 IrreflexiveObjectProperty(<RO_0002350>),
 EquivalentObjectProperties(<RO_0002351> ObjectInverseOf(<RO_0002350>) )]

So it looks like the irreflexive object property axiom might be the key here - it should not be inferred for a non simple property, which RO_0002350 seems to be, but the property is not matched as non simple until the equivalent and subproperty axioms are added ('non simple property' is a syntactic check at this point).

[sesuncedu]

IrreflexiveObjectProperty can be informative and is common since it is entailed by disjoint range and domain. It's also a profile hazard.

[sesuncedu]

I wonder if anonymous inverse properties are "interesting" enough to be worth generating in inferred axioms. I'm assuming they mostly come directly from asserted named inverses.

not relevant, but is there a cite that explains the simple / complex property distinction on decidability? It would seem that the OWL rule is conservative in blocking the vacuous and trivial cases (there's quite a few places in the profiles where construct is completely blocked but could be allowed in small doses - e.g. ELK allows a few non-EL constructs that are syntactic equivalents of EL constructs).

[sesuncedu]

Re: redundant inferred axioms If an inferred axiom and a told axiom are logically equivalent, there are two possibilities:

1. The inferred axiom is redundant.
2. The told axiom is redundant.

The told axiom is redundant if the inferred axiom can be inferred from the ontology with the told axiom retracted. Otherwise, the inferred axiom is redundant.

The check can be expensive for things like SubClassOf, because it bypasses the fast path, and the checks can't readily be batched (though I think atoms can be checked in parallel).

[sesuncedu]

It can be useful to add annotations to inferred axioms with OWLAPI version, reasoner version, and told ontology version (or logical axiom hash). The annotation object can be reused. Annoyingly, individuals used as the value of annotations are visible to reasoners.

[alanruttenberg]

The value of annotations can be URIs that are not entities and so invisible to the reasoner.

[sesuncedu]

Checking for non-presence of an axiom, ignoring annotations, can be made faster without requiring excessive amounts of extra memory by using a bloom filter populated from the axiom set. The full check for hits can still be slow, and it doesn't work well if there are too many committed deletions.

I think I implemented this at one point during indexing experiments. Conveniently, Guava comes with probabilistic sets.

[sesuncedu]

The problem with annotation values becoming real is when the use case is perfect for an anonymous individual, or if you want to use non annotation property assertions on it without pulling it in. skos and skos-xl form a good example / horrible warning

[alanruttenberg]

Re: redundant inferred axioms If an inferred axiom and a told axiom are logically equivalent, there are two possibilities:

The inferred axiom is redundant. The told axiom is redundant.

Wouldn't the second case be that they are both redundant?

Regarding your last comment, yes, I agree. (I generally stay away from SKOS)

So if I understand the current analysis, the non-trivial aspect of the bug is that there can be more than one inferred axiom that together cause a violation of the restriction, though neither alone do? I'll have to wrap my head around that one.

On the point that the restrictions are too restrictive (e.g. entailed irreflexive property) that struck me as well. If it's entailed then it's as good as being there. I expect that the rationale for this is that the test can no longer be implemented as a syntactic test, and that allowing the test to involve reasoning might be too expensive.

[ignazio1977]

the non-trivial aspect of the bug is that there can be more than one inferred axiom that together cause a violation of the restriction, though neither alone do

Something along those lines. Basically, the generators are checking entailment of their local candidate against the totality, but not whether it fits with the other generated axioms.

I did not expect this to be a problem - because of monotonicity, if O entails ax1 and O entails ax2, I expected O U ax1 to also entail ax2 and the reverse. Especially for things like object property characteristics - but it appears that's not the case.

This is a composite bug (pun intended) - there are a couple of obvious OWLAPI misfirings, which I will be fixing shortly, and something more complex to deal with entailments - all entailments are equal, except the equaler one.

the test can no longer be implemented as a syntactic test, and that allowing the test to involve reasoning might be too expensive.

That's a risk, yes. My operating assumption is that checking if a property is non simple with a reasoner is still doable; lacking that, one could test the number of unsatisfiable classes before and after the generation, and if that number changes the added object characteristics can be rolled back.

[alanruttenberg]

I've got to the stage where I'm getting unsatisfiable classes; when looking for explanations, I've found the following exception coming up:

Exception in thread "main" java.lang.IllegalArgumentException: Non-simple property 'http://purl.obolibrary.org/obo/RO_0002351' or its inverse appears in irreflexive object property axiom. at org.semanticweb.HermiT.structural.ObjectPropertyInclusionManager.rewriteAxioms(ObjectPropertyInclusionManager.java:108) at org.semanticweb.HermiT.structural.OWLClausification.preprocessAndClausify(OWLClausification.java:163)

This doesn't make sense to me. If you've got unsatisfiable classes, then you've already satisfied the global restrictions. That looks like a bug in how explanation works.

I can see how inferred axioms could interact to violate the restrictions. However I don't see how, if they don't violate the global restrictions, they could be incompatible. Starting with O, axioms A is entailed if it is true in all models of O. Axiom B is entailed if it is true in all models of O. So in every model of O, both A and B are true. Therefore the conjunction is true in all models. The thing is that the models are defined by O. Adding A or B doesn't change the set of models.

Does that make sense?

[ignazio1977]

This doesn't make sense to me. If you've got unsatisfiable classes, then you've already satisfied the global restrictions. That looks like a bug in how explanation works.

I can't figure out why an exception is being thrown during explanation and not during regular reasoning either. Explanation works by starting from a basic set of axioms and adding one axiom at a time for debugging purposes; I would have expected the same exceptions in both situations.

This might depend on the reasoner implementation as well - such exceptions might be treated differently during initial loading and during handling of ontology updates.

[ignazio1977]

However the error message is providing me with a clue: Non-simple property 'http://purl.obolibrary.org/obo/RO_0002351'or its inverseappears in irreflexive object property axiom.

So far the code in the generators checks only if the property is simple, not its inverse - and this points to the fact that adding subproperties and equivalent properties to inverses is the problem, as it potentially makes the inverse of a property non simple. So, before saying p equivalentTo inv(s), I need to check that p is simple.

The fact that, clearly, the axioms are entailed in both cases, points out that this restriction is checked as a syntactic restriction only and not properly reasoned over, I think. Otherwise, it should kick off whether the axioms are asserted or not.

[alanruttenberg]

That sounds right. I'm still worried about the unsatisfiable classes issue. If the ontology violated the restrictions then it never should have got to checking satisfiability. If it did't violate restrictions then an added inference caused classes (and properties) to be unsatisfiable.

[ignazio1977]

If it did't violate restrictions then an added inference caused classes (and properties) to be unsatisfiable.

Yes that worries me too. I've tried only one reasoner, but it sounds like the axioms added should not all have been found to be entailed - or, it shows that the rules about disallowing non simple properties in certain contexts are overly restrictive.

[alanruttenberg]

Maybe would show that the rules leak. Ontology that should be considered as violating, was not?

[alanruttenberg]

So is there something akin to blame in the OWLAPI? I'm thinking that to debug https://github.com/owlcs/owlapi/issues/646#issuecomment-289571634 a binary search adding different sets of axioms that differ between (1) and (2) in https://github.com/owlcs/owlapi/issues/646#issuecomment-289158896 could be used to try to narrow down why the unsats happen.

[ignazio1977]

The explanation code in OWLAPI works kind of like bisecting commits to find which one introduced a bug - but the state of the art implementation is in the owlexplanation project, that Matthew developed for his PhD. https://github.com/matthewhorridge/owlexplanation

[neurorepro]

Hello, my apologies for jumping into this discussion years later, but i am facing what looks like a similar problem with the Collections Ontology. It does not seem logically consistent after running a reasoner on a version including both stated and inferred axioms.

The error is "Non-simple object property 'http://purl.org/co/itemOf' is used as a simple one", and i created an issue here on that subject but the repository looks no longer maintained.

This is a complete roadblock at this point, and i was wondering if you had any luck with solving the issue you were facing ? I believe that in our case the Collections Ontology is quite smaller but we still couldn't fix the problem.

[alanruttenberg]

I wasn't generating the inferred version using Protege, instead using the OWLAPI directly. To avoid the issue I stopped including some kinds of inferred axioms.

I think that will work in your case too. To test, I loaded collections.owl, used FaCT++ as the reasoner (HermiT throws an error about some SWRL problem) and verified that if I deselect Object Property Characteristics, Data Property Characteristics, and Inverse Object Properties in the "Select axioms to export" dialog then I don't get the error you are getting, but if they are selected I do get it. So give that a try.

[neurorepro]

@alanruttenberg can't thank you enough for this, thank you so much for taking time to test it !

[neurorepro]

@alanruttenberg Thanks to your indications and after some digging, deselecting Object Property Characterists turned to be enough luckily !

Doing a diff with the full export provides the output below. It seems the error was due to properties being both asymmetric and irreflexive.

So would you say that the initial ontology was logically inconsistent, or that a problem was with the reasoners (at least Pellet and Fact++ in this case) ?

###  http://purl.org/co/item
<http://purl.org/co/item> rdf:type owl:ObjectProperty ;
                          owl:inverseOf <http://purl.org/co/itemOf> ;
-                          rdf:type owl:AsymmetricProperty ,
-                                   owl:IrreflexiveProperty ;
                          rdfs:domain <http://purl.org/co/Bag> ;
                          rdfs:range <http://purl.org/co/Item> ;
                          owl:propertyChainAxiom ( <http://purl.org/co/item>
                                                   <http://purl.org/co/nextItem>
                                                 ) ;
                          rdfs:comment "The link to every item of the bag"@en ;
                          rdfs:label "has item"@en .

and

###  http://purl.org/co/itemOf
+<http://purl.org/co/itemOf> rdf:type owl:ObjectProperty ;
-<http://purl.org/co/itemOf> rdf:type owl:ObjectProperty ,
-                                     owl:AsymmetricProperty ,
-                                     owl:IrreflexiveProperty ;
                            rdfs:comment "The link to a bag in which the item is member."@en ;
                            rdfs:label "is item of"@en .

[alanruttenberg]

The problem is with the way that the inferred axioms are being generated. It's not that the ontology is inconsistent. Rather it's that if the inferred axiom is added, the resultant ontology isn't OWL DL. Since it isn't OWL DL, the reasoner can't even try to check consistency.

In order for an OWL DL ontology to be syntactically valid there are combinations of axioms that aren't allowed. That's because if they were allowed they would make reasoning undecidable. Whether such combinations arise as a result of there being an inferred axiom isn't adequately checked.

The relevant part of the spec is Global Restrictions on Axioms in OWL 2 DL. It's kind of a difficult to understand the way it is presented but the short story is that properties are classified as simple or not. In an example in the spec it says:

Roughly speaking, a simple object property expression has no direct or indirect subproperties that are either transitive or are defined by means of property chains, where the notion of indirect subproperties is captured by the property hierarchy.

In your case it looks to me like is item of is non-simple because there's a property chain involving it's inverse has item. But an assertion of asymmetry or irreflexivity, which the inferred axiom generators produce, can only be made on a simple property. Whoops.

It's a bug that this happens. In the discussion above, a number of cases where this situation might arise were fixed but apparently not all of them.

[neurorepro]

Thank you very much for the explanation. At this high level it makes sense to me.

Then would it be right to say that an ontology isn't OWL DL if it is not OWL DL when inferred axioms are added ? So in this case is the bug in the Collections Ontology we were looking at, which is then not OWL DL ?

Or it is OWL DL but the bug is in the axiom generation process as the inferred axioms should not have been generated on a non-simple property ? If it is the latter and it is a bug, then would you know from which software component is it and how I should report it ?

[alanruttenberg]

The second. Your ontology is OWL-DL and this is a bug. The bug is either in the current OWLAPI or in the version of the OWLAPI that Protege is using. This is the appropriate thread for the OWLAPI issue. Perhaps @ignazio1977 can have a look and decide whether it is fixed in the current OWLAPI and @matthewhorridge, who maintains Protege, could review whether Protege needs an OWLAPI update.

[ignazio1977]

I remember a patch set written by @sesuncedu which was intended to address something very similar in inferred axioms - not sure whether it was intended for this exact scenario or not.

Here these axioms shouldn't be added to the ontology, but I'm puzzled by whether they are correctly inferred in the first place. Certainly if they're correctly inferred then the ontology cannot be used for reasoning, as it's not OWL DL, in which case how can they be inferred?

Considering it a purely syntactic restriction (i.e., infer, but don't materialise), the fix would be having two generators, one for use during materialisation and one for other uses. The first would ignore such axioms.