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

Hi Jos and Patrick,
Thanks for the answer and explanation. That helps a lot.
Sure, not able to provide all three is understandable. Apologise I’m not a logician in that sense and didn’t realise that was the reason.

Anyway, hope this can be supported, as it does seem like a useful case.

In the meantime, I’m playing around with N3 built-ins to overcome/workaround this issue. At the moment I’m using lists and relevant built-ins as a workaround. Not as natural, but works for my case for now.
While doing that, I also tried to use log:equalTo, but didn’t work either. Seems like it’s related to how formulas are restructured after loading the reasoner. Not an expert, but probably because they are separated as two goals in Prolog and then evaluated (thus assigned/unified) separately.

Best,
Rui

On 29 Aug 2023, at 23:37, Jos De Roo <josderoo@gmail.com> wrote:

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<https://josd.github.io/>


On Mon, Aug 28, 2023 at 5:33 PM Rui Zhao <rui.zhao@cs.ox.ac.uk<mailto: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