-
-
-
## About
-This is a re-implementation of the combined approach for CQ answering over RSA ontologies described in [[1](#references)].
+This is an *improved* re-implementation of the combined approach for CQ answering over RSA ontologies described in [[1](#references)].
-> Please note that the prototype mentioned in [[1](#references)] is not available (and the contributors of this repository have never seen it);
+> Please note that the prototype mentioned in [[1](#references)] is not available (and the contributors to this repository have never seen it);
> therefore, this "re-implementation" could be completely different from that prototype (potentially using different tools and programming language).
## Preliminaries
@@ -68,7 +47,58 @@ In order to use this program you need to have [RDFox](https://www.oxfordsemantic
RDFox is proprietary software and as such we are not able to distribute it along with our code.
Please refer to [this link](https://www.oxfordsemantic.tech/tryrdfoxforfree) to request a free trial.
-This software has been developed and tested with RDFox v.4.1
+This software has been developed and tested with RDFox v5.2.1
+
+## 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 are using different tools to carry out reasoning tasks and we are probably using a different language to implement the system.
+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.
+
++ âš¡ The system accepts unrestricted OWL ontologies as input and takes care of normalising and approximating the ontology to RSA.
+ At the time of writing, two approximation algorithms are provided, to compute a sound (or complete) set of answer to the input queries, respectively.
+
++ âš¡ The different steps of the combined approach (namely, the canonical model computation and the filtering step) are executed in isolation using different *named graphs*.
+ This allows us to reuse partial products of the computation and can even be used to parellalise filtering and answering 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
+
+ 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:
+ ```
+ owl:Thing[?X1], ..., owl:Thing[?Xn] :- p(?X1, ..., ?Xn) .
+ ```
+ Note that, by definition, arity can be either 1 or 2.
+
++ 🔄 Equality axiomatisation is performed introducing the following rules:
+ ```
+ rsacomb:congruent[?X, ?X] :- owl:Thing[?X] .
+ rsacomb:congruent[?Y, ?X] :- rsacomb:congruent[?X, ?Y] .
+ rsacomb:congruent[?X, ?Z] :- rsacomb:congruent[?X, ?Y], rsacomb:congruent[?Y, ?Z] .
+ ```
+ defining equivalence as a congruence relation over terms in the ontology.
+ Substitution rules propagate the equivalence to all existing atoms.
+
++ 🔧 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:
+ ```
+ 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.
+
++ âš¡ 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.
## Using the software
@@ -79,9 +109,9 @@ Download links for specific versions and operating systems can be found [here](h
```{.bash}
mkdir -p lib && pushd lib
-wget https://rdfox-distribution.s3.eu-west-2.amazonaws.com/release/v4.2.0/RDFox-linux-4.2.0.zip
-unzip RDFox-linux-4.2.0.zip
-ln -s RDFox-linux-4.2.0.zip/lib/JRDFox.jar
+wget https://rdfox-distribution.s3.eu-west-2.amazonaws.com/release/v5.2.1/RDFox-linux-x86_64-5.2.1.zip
+unzip RDFox-linux-x86_64-5.2.1.zip
+ln -s RDFox-linux-x86_64-5.2.1.zip/lib/JRDFox.jar
popd
```
@@ -106,11 +136,7 @@ Run the following from the base directory of the project to produce a standalone
sbt assembly
```
-The output of the command will print the location of the produced jar. Execute it with
-```
-java -jar [