Throw exception on reasoner errs, and test RBox for incoherency

[cmungall]

• Throws exceptions if ontology logically incoherent, fixes Signaling of fatal/blocking errors #40
• Includes incoherent OPs in logical tests, fixes test for unsatisfiable ObjectProperties #104

Note that the output is somewhat unfriendly, e.g.

$ robot materialize -i ./robot-core/src/test/resources/incoherent-rbox.owl 
ERROR There are 1 unsatisfiable properties in the ontology.
ERROR     unsatisfiable property: http://x.org/Q
org.obolibrary.robot.exceptions.IncoherentRBoxException
        at org.obolibrary.robot.ReasonerHelper.validate(ReasonerHelper.java:98)
        at org.obolibrary.robot.MaterializeOperation.materialize(MaterializeOperation.java:132)
        at org.obolibrary.robot.MaterializeOperation.materialize(MaterializeOperation.java:85)
        at org.obolibrary.robot.MaterializeCommand.execute(MaterializeCommand.java:168)
        at org.obolibrary.robot.CommandManager.executeCommand(CommandManager.java:242)
        at org.obolibrary.robot.CommandManager.execute(CommandManager.java:177)
        at org.obolibrary.robot.CommandManager.main(CommandManager.java:135)
        at org.obolibrary.robot.CommandLineInterface.main(CommandLineInterface.java:54)
usage: robot [command] [options] <arguments>
 -h,--help                  print usage information
 -noprefixes                do not use default prefixes
 -p,--prefix <arg>          add a prefix 'foo: http://bar'
 -P,--prefixes <arg>        use prefixes from JSON-LD file
 -V,--version               print version information
 -v,--verbose               increased logging
 -vv,--very-verbose         high logging
 -vvv,--very-very-verbose   maximum logging
 -x,--xml-entities          use entity substitution with ontology XML
                            output
commands:
 help             print help for command
 annotate         annotate ontology
 convert          convert ontology
 diff             find the differences between two ontologies
 export-prefixes  export prefixes to a file
 extract          extract terms from an ontology
 filter           filter ontology axioms
 materialize      materialize ontology
 merge            merge ontologies
 query            query an ontology
 reason           reason ontology
 reduce           reduce ontology
 relax            relax ontology
 template         build an ontology from a template
 unmerge          unmerge ontologies
 validate-profile validate ontology against an OWL profile

but being unfriendly is better than silently progressing with an incoherent ontology

[cmungall]

@jamesaoverton, @balhoff - does this look OK?

[balhoff]

+1

[jamesaoverton]

+1

[balhoff]

I said it looks okay, but now it's getting in my way. :-) I'm trying to use the expression-materializing-reasoner to materialize the go-graphstore tbox, but getting:

ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_16665
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_17996
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_16664
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_17995
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_16663
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_17994
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_28637
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30946
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30948
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30942
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30944
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/GO_0031088
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/GO_0031089
ERROR     unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_28631
org.obolibrary.robot.exceptions.IncoherentTBoxException

I feel like this should be ignorable, and we should let the user proceed if they want. The output would still be useful even though I'm not in a position to fix these right now.

[cmungall]

Are you sure you want to proceed given incoherency? Note that unsats will be inferred to be subclasses of all (satisfiable) classes in the ontology. Even if we filtered this inference in robot, downstream inferences could re-introduce it. This would be massively confusing to users. In owltools we provide two repair mechanisms: 1. remove any unsat classes 2. weaken the ontology by removing disjointness etc. E.g. owltools foo.owl --remove-axioms -t DisjointClasses The latter seems justifiable here.

…

On 17 Feb 2017, at 7:42, Jim Balhoff wrote: I said it looks okay, but now it's getting in my way. :-) I'm trying to use the expression-materializing-reasoner to materialize the go-graphstore tbox, but getting: ``` ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_16665 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_17996 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_16664 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_17995 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_16663 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_17994 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_28637 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30946 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30948 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30942 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_30944 ERROR unsatisfiable: http://purl.obolibrary.org/obo/GO_0031088 ERROR unsatisfiable: http://purl.obolibrary.org/obo/GO_0031089 ERROR unsatisfiable: http://purl.obolibrary.org/obo/EMAPA_28631 org.obolibrary.robot.exceptions.IncoherentTBoxException ``` I feel like this should be ignorable, and we should let the user proceed if they want. The output would still be useful even though I'm not in a position to fix these right now. -- You are receiving this because you modified the open/close state. Reply to this email directly or view it on GitHub: #133 (comment)

[balhoff]

Right, I think 2 is better. I looked for it in ROBOT but I guess it's not available. Is this general enough to have in ROBOT?

[jamesaoverton]

(If I'm understanding correctly) I think that an operation (or option on an operation) to remove disjointness axioms would be a good addition to ROBOT.

[cmungall]

Yes, I'd do it the owltools way where the axiom type is a parameter, as 'removed-disjointness-axiom' is very specific and not very verb-y We already have 'filter' but that may be overloading?

…

On 17 Feb 2017, at 10:52, James A. Overton wrote: (If I'm understanding correctly) I think that an operation (or option on an operation) to remove disjointness axioms would be a good addition to ROBOT. -- You are receiving this because you modified the open/close state. Reply to this email directly or view it on GitHub: #133 (comment)

[jamesaoverton]

Naming is hard, and ROBOT's filter command is not as general as its name implies. Still, I think thatfilter should be positive, as in "these are the things I want to keep". For the proposed operation I'd suggest remove, which would be negative: "these are the things that I don't want to keep". At least that matches the usage in functional programming language, such as Clojure.