Re: working with Skolem IRIs

I have given this some more thought, and my opinion right now is that : 
blank node inside quoted formulae should not be mapped by a variable, 
not skolemize.

My understanding of skolemization is, in a nutshell: "if such a thing 
exist, then you can pick one at random, and name it".

But this does not apply to existentials in quoted formulae, because 
quoted formulae are not taken for granted by the reasoner, and so 
neither is the existence of the things those formulae are about.

Consider the following:

   :alice :claims { [] a :Unicorn }.

Even if Alice is convinced that there exist a unicorn, we are not, so we 
can not pretend to pick one and name it.

So I don't like, in test2.n3, the fact that EYE replaces _:x with a 
skolem IRI.

---

For the same reason, I think that variables should *not* match a blank 
node in a nested formula... Such blank node does not denote anything 
that exist (at least, as far as the reasoner is concerned).

So I don't like either the conclusion for test3.n3, where the blank node 
in the quoted formula finds its way back as an existential in the global 
scope (there is a thing that we like).

   pa


On 08/06/2021 18:54, Jos De Roo wrote:
> Ooops..
> The 3rd case should have been
>
> $ cat test3.n3
> @prefix : <https://example.org/ns/example# 
> <https://example.org/ns/example#>> .
>
> :we :doubt { _:x a :Unicorn }.
> :we :doubt { :rex a :Unicorn }.
>
> @forAll :x.
> { :we :doubt { :x a :Unicorn } } => { :we :wish { :x a :Unicorn } }.
>
> $ eye --quiet --nope test3.n3 --pass 2> /dev/null
> PREFIX : <https://example.org/ns/example# 
> <https://example.org/ns/example#>>
>
> :we :doubt 
> {<http://josd.github.io/.well-known/genid/oiYDWzZAZyTTWrZsgJjysvBz7cY#e_x_1 
> <http://josd.github.io/.well-known/genid/oiYDWzZAZyTTWrZsgJjysvBz7cY#e_x_1>> 
> a :Unicorn}.
> :we :doubt {:rex a :Unicorn}.
> :we :wish 
> {<http://josd.github.io/.well-known/genid/oiYDWzZAZyTTWrZsgJjysvBz7cY#e_x_1 
> <http://josd.github.io/.well-known/genid/oiYDWzZAZyTTWrZsgJjysvBz7cY#e_x_1>> 
> a :Unicorn}.
> :we :wish {:rex a :Unicorn}.
>
>
> There are also some more eye corrections (esp. for rule generating rules)
> and the latest release is now 
> https://github.com/josd/eye/releases/tag/v21.0608.1647 
> <https://github.com/josd/eye/releases/tag/v21.0608.1647>
>
> Jos
>
> -- https://josd.github.io/ <http://josd.github.io/>
>
>
> On Tue, Jun 8, 2021 at 3:06 PM Jos De Roo <josderoo@gmail.com 
> <mailto:josderoo@gmail.com>> wrote:
>
>     Thanks for the constructive meeting yesterday
>     https://docs.google.com/document/d/1A3HAUhjaVnnJ6yVbFAvIBRJQjUY9aFlQ2_bGxkD0mnE/edit
>     <https://docs.google.com/document/d/1A3HAUhjaVnnJ6yVbFAvIBRJQjUY9aFlQ2_bGxkD0mnE/edit>
>     and ss discussed, I investigated the 3 test case
>     http://ppr.cs.dal.ca:3002/n3/editor/s/BCjsuKDM
>     <http://ppr.cs.dal.ca:3002/n3/editor/s/BCjsuKDM>
>
>     http://ppr.cs.dal.ca:3002/n3/editor/s/c3BNl6HQ
>     <http://ppr.cs.dal.ca:3002/n3/editor/s/c3BNl6HQ>
>
>     http://ppr.cs.dal.ca:3002/n3/editor/s/36y4Kyvc
>     <http://ppr.cs.dal.ca:3002/n3/editor/s/36y4Kyvc>
>
>     and made corrections in the latest eye release
>     https://github.com/josd/eye/releases/tag/v21.0608.1236
>     <https://github.com/josd/eye/releases/tag/v21.0608.1236>
>
>     In detail, the answers are now as follows:
>
>     $ cat test1.n3
>     Prefix : <https://example.org/ns/example#
>     <https://example.org/ns/example#>>
>
>     :tom a :Cat.
>     _:x a :Cat.
>
>     {?x a :Cat}=>{:we :doubt {?x a :Dog}}.
>
>     $ eye --quiet --nope test1.n3 --pass 2> /dev/null
>     PREFIX : <https://example.org/ns/example#
>     <https://example.org/ns/example#>>
>
>     :tom a :Cat.
>     _:e_x_1 a :Cat.
>     :we :doubt {:tom a :Dog}.
>     :we :doubt
>     {<http://josd.github.io/.well-known/genid/b2nrBWsoaecgOIC7KXr1yViiq:k#e_x_1
>     <http://josd.github.io/.well-known/genid/b2nrBWsoaecgOIC7KXr1yViiq:k#e_x_1>>
>     a :Dog}.
>
>     $ cat test2.n3
>     @prefix : <https://example.org/ns/example#
>     <https://example.org/ns/example#>> .
>
>     :we :doubt { _:x a :Unicorn }.
>     :we :doubt { :rex a :Unicorn }.
>
>     @forAll :x.
>     { :we :doubt { :x a :Unicorn } } => { :we :like :x }.
>
>     $ eye --quiet --nope test2.n3 --pass 2> /dev/null
>     PREFIX : <https://example.org/ns/example#
>     <https://example.org/ns/example#>>
>
>     :we :doubt
>     {<http://josd.github.io/.well-known/genid/Cq1oCASTEiQwLTKPixnecepqJCg#e_x_1
>     <http://josd.github.io/.well-known/genid/Cq1oCASTEiQwLTKPixnecepqJCg#e_x_1>>
>     a :Unicorn}.
>     :we :doubt {:rex a :Unicorn}.
>     :we :like _:e_x_1.
>     :we :like :rex.
>
>     $ cat test3.n3
>     @prefix : <https://example.org/ns/example#
>     <https://example.org/ns/example#>> .
>
>     :we :doubt { _:x a :Unicorn }.
>     :we :doubt { :rex a :Unicorn }.
>
>     @forAll :x.
>     { :we :doubt { :x a :Unicorn } } => { :we :like :x }.
>
>     $ eye --quiet --nope test3.n3 --pass 2> /dev/null
>     PREFIX : <https://example.org/ns/example#
>     <https://example.org/ns/example#>>
>
>     :we :doubt
>     {<http://josd.github.io/.well-known/genid/3qFbvxHHHzcCfeYYMoDVFV79S5g#e_x_1
>     <http://josd.github.io/.well-known/genid/3qFbvxHHHzcCfeYYMoDVFV79S5g#e_x_1>>
>     a :Unicorn}.
>     :we :doubt {:rex a :Unicorn}.
>     :we :like _:e_x_1.
>     :we :like :rex.
>
>
>     PS William, if fine, could you install the latest eye
>     https://github.com/josd/eye/releases/tag/v21.0608.1236
>     <https://github.com/josd/eye/releases/tag/v21.0608.1236>
>     at http://ppr.cs.dal.ca:3002/n3/editor/
>     <http://ppr.cs.dal.ca:3002/n3/editor/>
>     and BTw thanks for such a nice tool, it's really nice and useful!
>
>     -- https://josd.github.io/ <http://josd.github.io/>
>