Update README.md

1 files changed, 10 insertions, 7 deletions

diff --git a/README.md b/README.md
index d1de522..eb4657d 100644
--- a/README.md
+++ b/README.md
@@ -37,15 +37,18 @@ The following is a summary of fixes (🔧), changes (🔄) and improvements (⚡
 
 + 🔄 [RDFox](https://www.oxfordsemantic.tech/product) is used instead of DLV as the underlying LP engine.
 
-+ 🔧 In [[1](#references) - 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".
-    This has been fixed by (1) introducing a built-in predicate `In` (note that instances of `In` can be computed beforehand since they only depend on the input ontology), and (2) implement `notIn` as the negation of `In` using RDFox NaF built-in support.
++ 🔧 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
+
+    This has been fixed by (1) introducing a built-in predicate `In` (note that instances of `In` can be computed beforehand since they only depend on the input ontology), and (2) implement `notIn` as the negation of `In` using RDFox *NaF* built-in support.
 
 + 🔄 Top (`owl:Thing`) axiomatisation is performed introducing rules as follows.
-    Given *p* predicate (arity *n*) *in the original ontology*, the following rule is introduced:
+    Given `p` predicate (arity *n*) *in the original ontology*, the following rule is introduced:
     ```
-        owl:Thing[?X1], *...*, owl:Thing[?Xn] :- *p*(?X1, *...*, ?Xn) .
+        owl:Thing[?X1], ..., owl:Thing[?Xn] :- p(?X1, ..., ?Xn) .
     ```
-    Note that by definition arity can be either 1 or 2.
+    Note that, by definition, arity can be either 1 or 2.
 
 + 🔄 Equality axiomatisation is performed introducing the following rules:
     ```
@@ -56,12 +59,12 @@ The following is a summary of fixes (🔧), changes (🔄) and improvements (⚡
     defining equivalence as a congruence relation over terms in the ontology.
     *Substitution rules have not been entroduced yet.*
 
-+ 🔧 In [[1](#references) - Def. 4], the definition of built-in predicate `NI` is not consistent with its use in [[1](#references) - Table 3] and related description in [[1](#references) - Sec. 4.2].
++ 🔧 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`).
   Note that, in this scenario, there is no need to introduce `NI` instances as facts in the system;
   instead we can add a rule to populate the new predicate:
   ```
-    NI[?X] :- rsa:congruent[?X, ?Y], rsa:named[?Y] .
+    rsa:NI[?X] :- rsa:congruent[?X, ?Y], rsa:named[?Y] .
   ```
   where `rsa:named` is an internal predicate keeping track of all constants in the original ontology.