# Re: rule application proof step and existentials

From: <jos.deroo@agfa.com>
Date: Wed, 14 Feb 2007 10:44:32 +0100

Message-ID: <OF2D461328.8612F72E-ONC1257282.003520F1-C1257282.00357A92@agfa.com>
```
> Back in September,
> http://lists.w3.org/Archives/Public/public-cwm-talk/2006JulSep/0009.html
>
> I pointed out something wierd with this case:
> ---8<---
> @prefix : <gmpbnode#>.
> @keywords is, of, a.
>
> dan home [ in Texas ].
>
> { ?WHO home ?WHERE.
>   ?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.
>
> ---8<---
>
> Yosi fixed that problem, today, we think. (Yay!)
>
> But while he was at it, he came up with this twist:
>
> --8<--
> @prefix : <gmpbnode#>.
> @keywords is, of, a.
> dan a Man; home [].
> { ?WHO home ?WHERE.
>   ?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.
> { dan home ?WHERE} => {?WHERE in Texas} .
> --8<--
>
> "What should the proof look like?" He asked me. I thought
> I knew the answer:
>
> 1. ... by parsing.
> 2. dan home [], by extraction from 1
> 3. { dan home ?WHERE} => {?WHERE in Texas} . by extraction.
> 4. dan home [ in Texas] by rule on 3 applied to 2
> 5. ... => { ?WHO homeRegion ?REGION }. by extraction from 1
> 6. dan homeRegion Texas by rule from line 5 applied to 4
> QED.
>
>
> But it's more subtle than that.
>
> We're pretty sure the proof can't actually be expressed
> using the structures we've been working with so far.
>
> I'm curious about what Euler does in this case.

all I can do at this moment is a quick run and will check later
.euler5
http://localhost/.euler+--prolog+temp/gmpbnode2.n3+--think+--filter+temp/gmpbnodeF.n3
yielding

[ a r:Proof, r:Conjunction;
r:component [ a r:Inference; r:gives {:dan :homeRegion :Texas};
r:evidence (
[ a r:Extraction; r:gives {:dan :homeRegion :Texas}; r:because [ a
r:Inference; r:gives {:dan :homeRegion :Texas}; r:evidence (
[ a r:Extraction; r:gives {@forSome var:e24637076_40_. :dan :home
var:e24637076_40_}; r:because [ a r:Parsing; r:source
<file://temp/gmpbnode2.n3>]]
[ a r:Extraction; r:gives {@forSome var:e24637076_40_.
var:e24637076_40_ :in :Texas}; r:because [ a r:Inference; r:gives
{@forSome var:e24637076_40_. var:e24637076_40_ :in :Texas}; r:evidence (
[ a r:Extraction; r:gives {@forSome var:e24637076_40_. :dan :home
var:e24637076_40_}; r:because [ a r:Parsing; r:source
<file://temp/gmpbnode2.n3>]]);
r:binding [ r:variable [ n3:uri "http://localhost/var#WHERE"];
r:boundTo [ a r:Existential; n3:nodeId
"http://localhost/var#e24637076_40_"]];
r:rule [ a r:Extraction; r:gives {@forAll var:WHERE. {:dan :home
var:WHERE} => {var:WHERE :in :Texas}. }; r:because [ a r:Parsing; r:source
<file://temp/gmpbnode2.n3>]]]]);
r:binding [ r:variable [ n3:uri "http://localhost/var#WHO"];
r:boundTo [ n3:uri "file://temp/gmpbnode#dan"]];
r:binding [ r:variable [ n3:uri "http://localhost/var#WHERE"];
r:boundTo [ a r:Existential; n3:nodeId
"http://localhost/var#e24637076_40_"]];
r:binding [ r:variable [ n3:uri "http://localhost/var#REGION"];
r:boundTo [ n3:uri "file://temp/gmpbnode#Texas"]];
r:rule [ a r:Extraction; r:gives {@forAll
var:WHO,var:WHERE,var:REGION. {var:WHO :home var:WHERE. var:WHERE :in
var:REGION} => {var:WHO :homeRegion var:REGION}. }; r:because [ a
r:Parsing; r:source <file://temp/gmpbnode2.n3>]]]]);
r:binding [ r:variable [ n3:uri "http://localhost/var#WHO"]; r:boundTo
[ n3:uri "file://temp/gmpbnode#dan"]];
r:binding [ r:variable [ n3:uri "http://localhost/var#REGION"];
r:boundTo [ n3:uri "file://temp/gmpbnode#Texas"]];
r:rule [ a r:Extraction; r:gives {@forAll var:WHO,var:REGION. {var:WHO
:homeRegion var:REGION} => {var:WHO :homeRegion var:REGION}. }; r:because
[ a r:Parsing; r:source <temp/gmpbnodeF.n3>]]];
r:gives {
:dan :homeRegion :Texas.}].

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
```
Received on Wednesday, 14 February 2007 09:44:54 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:01:05 UTC