Add exclude-tautologies option for reason command.

docs/reason.md

@@ -73,6 +73,18 @@ The `<arg>` options are:
  * `all`: always allow (default behavior)
  * `none`: never allow
  * `asserted-only`: allow asserted equivalence, but throw an error if equivalence is inferred
+
+## Excluding tautologies
+
+A **tautology** is an axiom that would be true in any ontology, i.e., it's just a given due to the semantics of OWL. For example, every class is a subclass 
+of `owl:Thing`; it is not generally useful for an ontology to explicitly state this. Some reasoners may however include these kinds of statements as part 
+of their output. The ROBOT `reason` command provides an option for filtering out tautologies generated by the reasoning process: `--exclude-tautologies <arg>`.
+
+The options for `<arg>` are:
+
+ * `false` (default): allow any generated tautologies in the output.
+ * `all` (recommended): use the HermiT reasoner to exclude any inferred axioms that would be entailed by an empty ontology.
+ * `structural` (fast): exclude axioms matching a hard-coded set of tautological patterns (e.g., `X SubClassOf owl:Thing`, `owl:Nothing SubClassOf X`, `X SubClassOf X`). Much faster than `all`.
 
 ## Generated Axioms
 

robot-command/src/main/java/org/obolibrary/robot/ReasonCommand.java

@@ -70,6 +70,11 @@ public ReasonCommand() {
         "exclude-external-entities",
         true,
         "if true, do not add an axiom if it is about classes in external ontologies");
+    o.addOption(
+        "t",
+        "exclude-tautologies",
+        true,
+        "specify approach for excluding tautologies: 'structural' (fast), 'all' (use HermiT, slower), 'false' (allow tautologies)");
     o.addOption("T", "exclude-owl-thing", true, "if true, exclude inferences to owl:Thing");
     o.addOption(
         "e",

robot-core/src/main/java/org/obolibrary/robot/ReasonOperation.java

@@ -11,6 +11,7 @@
 import org.obolibrary.robot.reason.EquivalentClassReasoning;
 import org.obolibrary.robot.reason.EquivalentClassReasoningMode;
 import org.obolibrary.robot.reason.InferredSubClassAxiomGeneratorIncludingIndirect;
+import org.semanticweb.HermiT.ReasonerFactory;
 import org.semanticweb.owlapi.apibinding.OWLManager;
 import org.semanticweb.owlapi.model.*;
 import org.semanticweb.owlapi.model.parameters.Imports;
@@ -56,6 +57,7 @@ public static Map<String, String> getDefaultOptions() {
     options.put("dump-unsatisfiable", null);
     options.put("axiom-generators", "subclass");
     options.put("include-indirect", "false");
+    options.put("exclude-tautologies", "false");
 
     return options;
   }
@@ -350,7 +352,8 @@ private static void maybeCreateNewOntology(OWLOntology ontology, Map<String, Str
    * @param options Map of reason options
    */
   private static void addInferredAxioms(
-      OWLOntology ontology, OWLOntology newAxiomOntology, Map<String, String> options) {
+      OWLOntology ontology, OWLOntology newAxiomOntology, Map<String, String> options)
+      throws OWLOntologyCreationException {
     OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
     OWLDataFactory dataFactory = manager.getOWLDataFactory();
 
@@ -378,6 +381,16 @@ private static void addInferredAxioms(
       value = dataFactory.getOWLLiteral("true");
     }
 
+    // If we will need a tautology checker, create it only once
+    String tautologiesOption = OptionsHelper.getOption(options, "exclude-tautologies", "false");
+    OWLReasoner tautologyChecker;
+    if (tautologiesOption.equalsIgnoreCase("all")) {
+      OWLOntology empty = OWLManager.createOWLOntologyManager().createOntology();
+      tautologyChecker = new ReasonerFactory().createReasoner(empty);
+    } else {
+      tautologyChecker = null;
+    }
+
     // Look at each inferred axiom
     // Check the options, and maybe add the inferred axiom to the ontology
     for (OWLAxiom a : newAxiomOntology.getAxioms()) {
@@ -424,6 +437,43 @@ private static void addInferredAxioms(
         }
       }
 
+      if (tautologiesOption.equalsIgnoreCase("structural")) {
+        if (a instanceof OWLSubClassOfAxiom) {
+          OWLSubClassOfAxiom subClassOfAxiom = (OWLSubClassOfAxiom) a;
+          if (subClassOfAxiom.getSuperClass().isOWLThing()) {
+            continue;
+          } else if (subClassOfAxiom.getSubClass().isOWLNothing()) {
+            continue;
+          } else if (subClassOfAxiom.getSubClass().equals(subClassOfAxiom.getSuperClass())) {
+            continue;
+          }
+        } else if (a instanceof OWLEquivalentClassesAxiom) {
+          OWLEquivalentClassesAxiom equivAxiom = (OWLEquivalentClassesAxiom) a;
+          if (equivAxiom.getClassExpressions().size() < 2) {
+            continue;
+          }
+        } else if (a instanceof OWLClassAssertionAxiom) {
+          OWLClassAssertionAxiom classAssertion = (OWLClassAssertionAxiom) a;
+          if (classAssertion.getClassExpression().isOWLThing()) {
+            continue;
+          }
+        } else if (a instanceof OWLObjectPropertyAssertionAxiom) {
+          OWLObjectPropertyAssertionAxiom assertion = (OWLObjectPropertyAssertionAxiom) a;
+          if (assertion.getProperty().isOWLTopObjectProperty()) {
+            continue;
+          }
+        } else if (a instanceof OWLDataPropertyAssertionAxiom) {
+          OWLDataPropertyAssertionAxiom assertion = (OWLDataPropertyAssertionAxiom) a;
+          if (assertion.getProperty().isOWLTopDataProperty()) {
+            continue;
+          }
+        }
+      } else if (tautologiesOption.equalsIgnoreCase("all") && (tautologyChecker != null)) {
+        if (tautologyChecker.isEntailed(a)) {
+          continue;
+        }
+      }
+
       // If the axiom has not been skipped, add it to the ontology
       manager.addAxiom(ontology, a);
       // If propertyIRI isn't null, we are annotating the inferred axioms

robot-core/src/test/java/org/obolibrary/robot/ReasonOperationTest.java

@@ -11,6 +11,7 @@
 import org.semanticweb.elk.owlapi.ElkReasonerFactory;
 import org.semanticweb.owlapi.model.*;
 import org.semanticweb.owlapi.reasoner.OWLReasonerFactory;
+import org.semanticweb.owlapi.search.EntitySearcher;
 import uk.ac.manchester.cs.jfact.JFactFactory;
 
 /** Tests for ReasonOperation. */
@@ -150,6 +151,19 @@ public void testRemoveRedundantSubClassAxioms() throws Exception {
     assertIdentical("/without_redundant_subclasses.owl", reasoned);
   }
 
+  @Test
+  public void testExcludeTautologies() throws Exception {
+    OWLOntology input = loadOntology("/reason_exclude_tautologies.ofn");
+    OWLReasonerFactory reasonerFactory = new org.semanticweb.elk.owlapi.ElkReasonerFactory();
+    Map<String, String> options = new HashMap<>();
+    options.put("exclude-tautologies", "structural");
+    ReasonOperation.reason(input, reasonerFactory, options);
+    assertFalse(
+        EntitySearcher.getSuperClasses(
+                dataFactory.getOWLClass(IRI.create("http://example.org/B")), input)
+            .contains(dataFactory.getOWLThing()));
+  }
+
   /**
    * Test reasoning with Expression Materializing Reasoner.
    *

robot-core/src/test/resources/reason_exclude_tautologies.ofn

@@ -0,0 +1,29 @@
+Prefix(:=<http://example.org/>)
+Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
+Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>)
+Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)
+Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
+Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)
+
+
+Ontology(<http://example.org/>
+
+Declaration(Class(:A))
+Declaration(Class(:B))
+Declaration(Class(:C))
+Declaration(ObjectProperty(:r))
+
+############################
+#   Classes
+############################
+
+# Class: :A (:A)
+
+SubClassOf(:A ObjectSomeValuesFrom(:r :B))
+
+# Class: :C (:C)
+
+EquivalentClasses(:C ObjectSomeValuesFrom(:r :B))
+
+
+)