Re: rule application proof step and existentials

> 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