Re: working with Skolem IRIs

There is now a further fixing of Skolem IRIs in the latest version of eye
https://github.com/josd/eye/releases/tag/v21.0609.2221
and now Doerthe's example i.e. test1.n3 gives

$ cat test1.n3
Prefix : <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-all 2> /dev/null
PREFIX : <https://example.org/ns/example#>
PREFIX skolem: <
http://josd.github.io/.well-known/genid/3FJcG7xlxhzlhSd9ScAHjl8il9Y#>

:tom a :Cat.
skolem:e_x_1 a :Cat.
:we :doubt {:tom a :Dog}.
:we :doubt {skolem:e_x_1 a :Dog}.
{?U_0 a :Cat} => {:we :doubt {?U_0 a :Dog}}.

The other 2 tests are still giving the following answers:

$ cat test2.n3
@prefix : <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-all 2> /dev/null
PREFIX : <https://example.org/ns/example#>
PREFIX skolem: <
http://josd.github.io/.well-known/genid/oSmETLylsaSaXb6b_y0orScfEJ4#>

:we :doubt {skolem:e_x_1 a :Unicorn}.
:we :doubt {:rex a :Unicorn}.
:we :like skolem:e_x_1.
:we :like :rex.
{:we :doubt {?U_0 a :Unicorn}} => {:we :like ?U_0}.


$ cat test3.n3
@prefix : <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-all 2> /dev/null
PREFIX : <https://example.org/ns/example#>
PREFIX skolem: <
http://josd.github.io/.well-known/genid/f_FLLOk6:O4Vimu5RctgZrA4ovI#>

:we :doubt {skolem:e_x_1 a :Unicorn}.
:we :doubt {:rex a :Unicorn}.
:we :wish {skolem:e_x_1 a :Unicorn}.
:we :wish {:rex a :Unicorn}.
{:we :doubt {?U_0 a :Unicorn}} => {:we :wish {?U_0 a :Unicorn}}.


-- https://josd.github.io/ <http://josd.github.io/>


On Wed, Jun 9, 2021 at 11:17 PM Jos De Roo <josderoo@gmail.com> wrote:

> Yes indeed Pierre-Antoine and it is also what William suggested
> and what I also thought while implementing but there was an
> issue with it for rules that generate rules like A => (B => C) (*)
> I hope that later tonight a fix will be available :-)
>
> Jos
>
> (*) this is needed for Erchovian compilation like in
> https://github.com/josd/eye/tree/master/reasoning/preduction
> but also for some "creativity" experiments that we do in the context
> of what we learned from the excellent book of Chiara Marletto
> https://www.chiaramarletto.com/books/the-science-of-can-and-cant/
>
>
> -- https://josd.github.io/ <http://josd.github.io/>
>
>
> On Wed, Jun 9, 2021 at 10:42 PM Pierre-Antoine Champin <
> pierre-antoine.champin@ercim.eu> wrote:
>
>>
>> On 09/06/2021 20:38, David Booth wrote:
>> > On 6/9/21 8:44 AM, William Van Woensel wrote:
>> >> Thanks Jos, I updated the N3 editor :-)
>> >>
>> >> I do have a question about these solutions:
>> >>
>> >> E.g.,
>> >>
>> >> 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}.
>> >>
>> >> When treating the skolem-iri as a regular IRI, does this say that we
>> >> doubt that the thing "_:e_x_1", which we know is a Cat, is also a dog
>> >> (which is the goal, I think)?
>> >>
>> >> The RDF 1.1 mentions the following about skolem IRIs: "Systems may
>> >> wish to mint Skolem IRIs in such a way that they can recognize the
>> >> IRIs as having been introduced solely to replace blank nodes. This
>> >> allows a system to map IRIs back to blank nodes if needed."
>> >>
>> >> In the above case, should the system know that the skolem-iri
>> >> corresponds to the original blank node (and thus act accordingly)?
>> >> I.e., do both terms co-refer to the same resource? ..
>> >
>> > I don't think that line in the RDF 1.1 Semantics means that a Skolem
>> > IRI would be mappable back to the original blank node label.  I always
>> > interpreted it to mean simply that Skokem IRIs could be mapped back to
>> > a fresh set of blank nodes.
>> >
>> > Even if a particular system did retain the original blank node label
>> > in the Skolem IRI (to enable it to be mapped back to the original
>> > blank node label), I think the system would be on very shaky ground to
>> > assume that the *current* blank node label _:e_x_1 is intended to
>> > refer to the *same* blank node from which the Skolem IRI was
>> > originally generated.  I think the situation is analogous to loading
>> > two independent RDF files: the same blank node label appearing in both
>> > files should not be assumed to denote the same blank node, unless you
>> > have special information that clearly indicates that that is intended.
>>
>> +1 to what David wrote.
>>
>> The last line of the conclusion merely says "there is a thing (with a
>> funny name) that we doubt is a Dog.
>>
>> That particular thing can not be traced back to being a Cat, which is
>> probably missing if we intend to explain the reasoning steps:
>>
>>    There exists a Cat
>>
>>      hence
>>
>>    let's pick one and name it <http...#e_x_1> (i.e.skolemization)
>>
>>      hence
>>
>>    <http...#e_x_1> is a Cat
>>
>>      hence
>>
>>    we doubt that <http...#e_x_1> is a Dog (per the rule)
>>
>> So I guess I would vote to add
>>
>> <
>> http://josd.github.io/.well-known/genid/b2nrBWsoaecgOIC7KXr1yViiq:k#e_x_1>
>>
>> a :Cat.
>>
>>     (in addition or in replacement of _:e_x_1 a :Cat )
>>
>> in EYEs conclusion for this example.
>>
>> >
>> > Thanks,
>> > David Booth
>> >
>> >>
>> >>
>> >> William
>> >>
>> >>
>> >> On 2021-06-08 1:54 p.m., 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/>
>> >>>
>> >
>>
>>

Received on Wednesday, 9 June 2021 22:45:29 UTC