4 files changed, 12 insertions, 26 deletions

diff --git a/README.md b/README.md
index 55a4b01..7a9697e 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,7 @@ We assume you followed [these steps](https://docs.oxfordsemantic.tech/getting-st
 
 The [documentation](https://docs.oxfordsemantic.tech/features-and-requirements.html#license-key), describes several ways to provide the license to RDFox.
 
-One easy way is to put your license key in a file `RDFox.lic` in `$HOME/.RDFox/`, with adeguate read permissions for the user executing the program.
+One easy way is to put your license key in a file `RDFox.lic` in `$HOME/.RDFox/`, with adequate read permissions for the user executing the program.
 
 ### Compiling and running the project
 
@@ -48,21 +48,21 @@ Note that the fat jar file distributed with this repository excludes the RDFox a
 java -cp <path/to/JRDFox.jar>:<path/to/fat.jar> uk.ac.ox.cs.rsacomb.RSAComb [<option> ...]
 ```
 
-### Running tests and examples
+### Running tests
 
-TODO
+To run the suit of unit test provided along with the code run
+```
+sbt test
+```
 
 ## Changes introduced
 
 We tried to implement the system as close as possible to the theoretical description provided in [[1](#references)].
 Regardless, we had to deal with the fact that we where using different tools to carry out reasoning tasks and we where probably using a different language to implement the system.
-The following is a summary of fixes (🔧), changes (🔄) and improvements (⚡), we introduced along the way:
+The following is a (non exhaustive) summary of fixes (🔧), changes (🔄) and improvements (⚡), we introduced along the way:
 
 + 🔄 [RDFox](https://www.oxfordsemantic.tech/product) is used instead of DLV as the underlying LP engine.
 
-+ 🔄 While the system is described as a two-step process (computing the canonical model and applying the filtering program), the adoption of RDFox allows us to abstract from the underlying engine implementation.
-    Materialisation is handled by RDFox, possibly computing answers in one go, without splitting the process in two separate steps.
-
 + 🔧 In Def.4, the definition of built-in predicate `notIn` is wrong and should reflect the implicit semantics implied by the name, i.e.,
 
     > let [...] `notIn` be a built-in predicate which holds when the first argument is **not** an element of the set given as second argument
@@ -83,7 +83,6 @@ The following is a summary of fixes (🔧), changes (🔄) and improvements (⚡
         rsa:congruent[?X, ?Z] :- rsa:congruent[?X, ?Y], rsa:congruent[?Y, ?Z] .
     ```
     defining equivalence as a congruence relation over terms in the ontology.
-    *Substitution rules have not been entroduced yet.*
 
 + 🔧 In Def. 4, the definition of built-in predicate `NI` is not consistent with its use in Table 3 and related description in Sec. 4.2.
   We redefined `NI` as the set of all constants that are *equal* to a constant in the original ontology (according to the internal equality predicate `rsa:congruent`).
@@ -94,12 +93,13 @@ The following is a summary of fixes (🔧), changes (🔄) and improvements (⚡
   ```
   where `rsa:named` is an internal predicate keeping track of all constants in the original ontology.
 
-+ ⚡ In Def. 3, regarding the generation of the logic program used for the RSA checkk, only T5 axioms involving an unsafe role will introduce the internal predicates `PE` and `U`.
++ ⚡ In Def. 3, regarding the generation of the logic program used for the RSA check, only T5 axioms involving an unsafe role will introduce the internal predicates `PE` and `U`.
 
 + ⚡ Both in the canonical model and the filtering program computations, rules without a body are loaded into RDFox as facts.
 
 + ⚡ The `cycle` function introduced in Def.4 establishing the direction of the *unraveling* of loops is defined over triples `(A,R,B)`. We are currently limiting the triple only to those appearing in a T5 axiom `A ⊑ ∃R.B`. Note that this greatly limits the size of cycle for a given triple, and as a consequence limits the number of rules used to compute the canonical model.
 
+
 ## References
 
 [1] Feier, Cristina, David Carral, Giorgio Stefanoni, Bernardo Cuenca Grau, and Ian Horrocks.
@@ -109,12 +109,12 @@ The following is a summary of fixes (🔧), changes (🔄) and improvements (⚡
 
 ## Acknowledgements
 
-TODO
+*temporarily redacted*
 
 ## Credits
 
-TODO
+*temporarily redacted*
 
 ## License
 
-TODO
+*temporarily redacted*
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
index 3da6c8a..6621f59 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -118,10 +118,6 @@ class CanonicalModel(val ontology: RSAOntology) {
           .getIRI
         TupleTableAtom.rdf(v0, IRI.RDF_TYPE, cls)
       }
-      // TODO: To be consistent with the specifics of the visitor we are
-      // returning facts as `Rule`s with true body. While this is correct
-      // there is an easier way to import facts into RDFox. Are we able to
-      // do that?
       val facts = unfold map RSA.In
       val rules = List(
         Rule.create(roleRf, atomA, RSA.NotIn(varX)),
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
index 3527da5..c7b3bf0 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -459,7 +459,6 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
       Logger.DEBUG
     )
 
-  // TODO: the following functions needs testing
   def confl(
       role: OWLObjectPropertyExpression
   ): Set[OWLObjectPropertyExpression] = {
@@ -655,7 +654,6 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     // We just need the TBox to find
     val terms = for {
       axiom1 <- tbox
-      // TODO: is this an optimization or an error?
       if axiom1.isT5
       // We expect only one role coming out of a T5 axiom
       roleS <- axiom1.objectPropertyExpressionsInSignature
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
index c9bed35..3fac46f 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
@@ -23,13 +23,6 @@ import uk.ac.ox.cs.rsacomb.util.{RSA, RDFoxUtil}
   * @note the input axioms are assumed to be normalized. Trying to
   * convert non normalized axioms might result in undefined behavious.
   * We use the normalization defined in the main paper.
-  *
-  * @see [[https://github.com/KRR-Oxford/RSA-combined-approach GitHub repository]]
-  * for more information on the theoretical aspects of the system.
-  *
-  * @todo this is not ideal and it would be more sensible to prepend a
-  * normalization procedure that will prevent errors or unexpected
-  * results.
   */
 trait RDFoxConverter {
 
@@ -358,7 +351,6 @@ trait RDFoxConverter {
         */
       case e: OWLDataSomeValuesFrom => {
         val role = e.getProperty()
-        // TODO: simplify this:
         // Computes the result of rule skolemization. Depending on the used
         // technique it might involve the introduction of additional atoms,
         // and/or fresh constants and variables.