NI predicate

[dyamon]

This is just to keep track of the discussion about the instantiation of NI predicates in the RSA canonical model. In the paper NI in mentioned multiple times.

During the definition of canonical model for O:

[Definition 4] [...] Let P be the smallest program with a rule -> NI(a) for each constant a and all rules in Table 2 [...]

During the definition of filtering program:

[Table 3 - rules 3a, 5a, 5b, 5c]

we refer to all functional terms and Skolem constants in the model that are not equal to constant in O as anonymous

We keep track of identities in the model relative to a match using a fresh predicate id. It is initialised as the minimal congruence relation over the positions of the existential variables in the query which are mapped to anonymous terms (rules (3)).

Furthermore the predicate named is introduced in the filtering program seemingly with the same semantics.

---

At the time of writing we agreed on the following:

• predicate named is instantiated on all constants appearing in the original ontology O;
• Such predicates can be computed (in the code) before the filtering program, since they don't directly depend on the submitted query;
• predicate NI is defined as the set of constants in O along with any fresh constant introduced during the canonical model computation that are equivalent to a constant in O;
• given the canonical model we can retrieve all instances of NI with the following rule:

  NI(X) <- X rsa:EquivTo Y, named(Y).

---

Despite this decision we are still not sure why the paper introduces NI during the definition of the logic program used to compute the canonical model, since its instantiation depend on the canonical model itself.

[dyamon]

We decided to implement NIs using the following rule

NI(X) <- X rsa:EquivTo Y, named(Y).

[dyamon]

Note that removing NIs entirely from Def. 4 and from the computation of the canonical model might have an impact also on the theoretical results.

We need to check that Theorem 3 remains true even when removing the NI from Def. 4