Re: Existential Quantification [Re: New RDF model theory]

> In Pat's impressive document I note the following:

that's indeed very true

> As far as I can tell the following two graphs (which I represent in a
> bastardized ntriple) entail one another:
>
> G1:
> <a> <b> <c>.
>
>
> G2:
> <a> <b> <c>.
> _:x <b> <c>.
>
>
> Have I understood this right?
> If so, is this desired?

we've tried those entailments in both directions

//////////////////////////////////////////////////////////////
C:\n3>java Euler -core -trace jeremy1.nt jeremy2.nt
# <a> <b> <c>.
[1]CALL: <a> <b> <c>.
[1]EXIT: <a> <b> <c>.
[2]CALL: this log:forSome [ <b> <c>].
[2]EXIT: this log:forSome [ <b> <c>].
@@ continue
# Generated with Euler 27.045 on Fri Aug 17 11:35:09 CEST 2001
# for query file:/n3/jeremy2.nt
# given [file:/n3/jeremy1.nt]

@prefix log: <http://www.w3.org/2000/10/swap/log#>.

<a> <b> <c>.

# Proof found for file:/n3/jeremy2.nt in 2 steps (58 steps/sec)
\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

and

//////////////////////////////////////////////////////////////
C:\n3>java Euler -core -trace jeremy2.nt jeremy1.nt
# <a> <b> <c>.
# this log:forSome [ <b> <c>].
[1]CALL: <a> <b> <c>.
[1]EXIT: <a> <b> <c>.
@@ continue
# Generated with Euler 27.045 on Fri Aug 17 11:40:41 CEST 2001
# for query file:/n3/jeremy1.nt
# given [file:/n3/jeremy2.nt]

@prefix log: <http://www.w3.org/2000/10/swap/log#>.

<a> <b> <c>.

# Proof found for file:/n3/jeremy1.nt in 1 steps (54 steps/sec)
\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\

so they (indeed) entail each other...

> I am a little confused at the moment about it ...
>
> reading _:x <b> <c>. as existentially quanitifed then it seems trivial that
> G1 and G2 entail one another, whereas the interpolation lemma seems to be
> false.
>
> I might follow up on this later.

fine

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Friday, 17 August 2001 05:49:08 UTC