Re: (Deep-)Nested negative surfaces do not share blank nodes?

Fully agreed Patrick and it is a nice example.which fuels the evolution of
eye ;-)
EYE v4.14.10 (2023-08-30) now gives

@prefix skolem: <
http://eyereasoner.github.io/.well-known/genid/11a3f68e-7664-4d80-8143-4f28c06e78cc#
>.

<urn:example.org:Alice> a <urn:example.org:Person>.
_:sk_60 a <urn:example.org:Book>.
skolem:t_0 a <urn:example.org:Book>.
_:sk_60 <urn:example.org:borrowedBy> <urn:example.org:Alice>.
skolem:t_0 <urn:example.org:borrowedBy> <urn:example.org:Alice>.
<urn:example.org:Alice> <urn:example.org:created> <urn:example.org:
RDFHandBook>.
_:sk_62 <urn:example.org:discussed> <urn:example.org:RDFHandBook>.
skolem:t_0 <urn:example.org:discussed> <urn:example.org:RDFHandBook>.

Best,
Jos

-- https://josd.github.io


On Mon, Aug 28, 2023 at 5:33 PM Rui Zhao <rui.zhao@cs.ox.ac.uk> wrote:

> Hi,
>
> It’s very excited to see a reasoning mechanism with first-order logic
> capacity, on top of N3. RDF Surfaces got me very interesting, and I started
> to carefully learn it recently.
>
> I have read through the document, and a couple of examples in the
> repository. I have managed to encode most of my axioms using RDF Surfaces.
> However, I’m still having some difficulties on handling predicates with
> multiple objects.
>
> As an example, I would like to express the following formula:
>
> \forall X. A(X) —> \exists Y. (B(Y, X) /\ \forall Z. C(X, Z) —> D(Y, Z))
>
> The intuitive meaning is: for any A(X), we always have a Y such that B(Y,
> X); and if we have C(X, Z) for that X, we also have D(Y, Z) for that Y. My
> ABox originally only contains statements of A(X) and C(X, Z), and I want to
> use reasoner to derive information about Ys.
> Hope I didn’t make anything wrong with the logical formula.
>
> I tried to encode it using RDF Surfaces, and ended up with a series of
> nested negative surfaces, reflecting the following equivalent formula:
> NOT \exists X. (A(X) /\ NOT \exists Y. (B(Y, X) /\ NOT \exists Z. (C(X, Z)
> /\ NOT D(Y, Z)))
>
> For example, the following code illustrates my test case:
>
> ```
> @prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
> @prefix log: <http://www.w3.org/2000/10/swap/log#>.
> @prefix : <http://example.org/ns#>.
>
> :a a :Man.
> :a :knows :b.
>
> (_:x) log:onNegativeSurface {
>         _:x a :Man.
>         (_:y) log:onNegativeSurface {
>                 _:y a :Community;
>                         :contains _:x.
>                 (_:z) log:onNegativeSurface {
>                         _:x :knows _:z.
>                         () log:onNegativeSurface {
>                                 _:y :contains _:z.
>                         }.
>                 }.
>         }.
> }.
>
> (_:s _:p _:o) log:onQuerySurface {
>         _:s _:p _:o.
> }.
> ```
>
> I executed it with `eye --quiet --nope --blogic test-nested-neg2.n3s`.
> Result is:
>
> ```
> _:sk_21 a :Community.
> _:sk_21 :contains :a.
> _:sk_23 :contains :b.
> _:sk_24 :contains :c.
> ```
>
> (Other lines removed for clarify.)
>
> However, what I’m expecting is that the same :Community has all :a, :b and
> :c -- something like this:
>
> ```
> _:sk_21 a :Community.
> _:sk_21 :contains :a.
> _:sk_21 :contains :b.
> _:sk_21 :contains :c.
> ```
>
> Did I understand the semantics of RDF Surfaces incorrectly? How should I
> correctly express my formula?
>
> In particular, I think I may misunderstand something here:
> https://w3c-cg.github.io/rdfsurfaces/#Surface. It talks about the
> (co)reference of blank nodes, which says “...as coreferences to the blank
> node graffiti defined on a parent RDF Surface”. The “a parent” is a bit
> ambiguous to me. I understand this as “ (surfaces are nested as a tree,
> and) go up the surface tree branch from the current node/leaf, and find the
> nearest ancestor surface which contains a blank node with the same name
> (and use it)“. Is that correct?
>
> Any suggestion is appreciated.
>
> Best,
> Rui