Move exclude-tautologies doc to its own section.
@@ -35,10 +35,9 @@ robot reason --reasoner ELK \
--output results/reasoned.owl
```
-Finally, `reason` includes three more options to help clean the reasoned output:
+Finally, `reason` includes two more options to help clean the reasoned output:
* `--exclude-duplicate-axioms`: if set to true, the axioms will not be added to the output if they exist in an import (default `false`).
* `--remove-redundant-subclass-axioms`: if set to false, redundant axioms (those that have been asserted and were also inferred) are included in the output (default `true`).
-* `--exclude-tautologies`: if set to 'structural', exclude axioms matching a hard-coded set of tautological patterns (e.g., `X SubClassOf owl:Thing`, `owl:Nothing SubClassOf X`, `X SubClassOf X`); if 'all', use the HermiT reasoner to exclude any inferred axioms that would be entailed by an empty ontology; if 'false' (default), include any tautological inferences that may be asserted by an axiom generator.
If no `--reasoner` is provided, ROBOT will default to ELK. The following other reasoner options are supported:
@@ -75,6 +74,18 @@ The `<arg>` options are:
* `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`: allow any generated tautologies in the output.
+ * `all`: use the HermiT reasoner to exclude any inferred axioms that would be entailed by an empty ontology.
+ * `structural`: 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
By default, the `reason` operation will only assert inferred subclass axioms. This can be configured with the `--axiom-generators` option. OWLAPI provides the following inferred axiom generators:
