NI predicate
Opened this issue · 2 comments
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 constantaand 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
namedis instantiated on all constants appearing in the original ontologyO; - Such predicates can be computed (in the code) before the filtering program, since they don't directly depend on the submitted query;
- predicate
NIis defined as the set of constants inOalong with any fresh constant introduced during the canonical model computation that are equivalent to a constant inO; - given the canonical model we can retrieve all instances of
NIwith 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.
We decided to implement NIs using the following rule
NI(X) <- X rsa:EquivTo Y, named(Y).
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