This is summary of an attempt to generate a proof from a particular test case

Introduction

This is built around the test scenario described here:

@prefix : <gmpbnode#>.
@keywords is, of, a.

dan home [ in Texas ].

{ ?WHO home ?WHERE.
  ?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.

The diagrams below are rendered by FuXi, using its BGL Python binding library to render the proof and the RETE-UL network used to perform forward-chaining. This experimental code will soon be merged into FuXi. The diagram is annotated with the RIF BLD syntax

Euler Proof

For reference, below is the reason.n3 proof generated via euler:

[ 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.}].

Rendered Proof

Each Proof Step is a NodeSet and each justification (the range of the 'is consequence of' relation) is a InferenceStep

RETE-UL Network

Details

The console (while extracting proof from a goal and the evaluated RETE-UL network):

Forall ?REGION ?WHO ?WHERE dan:homeRegion(?WHO ?REGION) :- And( dan:home(?WHO ?WHERE) dan:in(?WHERE ?REGION) )
Forall ?WHERE dan:in(?WHERE dan:Texas) :- dan:home(dan:dan ?WHERE)
Time to build production rule (RDFLib): 0.00168204307556 seconds
[]
<Network: 2 rules, 6 nodes, 4 tokens in working memory, 2 inferred tokens>
Time to calculate closure on working memory:  9.73010063171 milli seconds
## Going in ##
[]
[dan:Man(dan:dan), dan:home(dan:dan _:TidWPjhF74)]
## Coming out ##
[dan:homeRegion(dan:dan dan:Texas), dan:in(_:TidWPjhF65 dan:Texas)]
goal  _4:homeRegion(_4:dan _4:Texas)
<Network: 2 rules, 6 nodes, 4 tokens in working memory, 2 inferred tokens>
Building nodeset around goal:  _4:homeRegion(_4:dan _4:Texas)
Building inference step for  Proof step for _4:homeRegion(_4:dan _4:Texas)
Inferred from <TerminalNode : CommonVariables: [?WHERE] (1 in left, 1 in right memories)> via _4:homeRegion(?WHO ?REGION) :- And( _4:home(?WHO ?WHERE) _4:in(?WHERE ?REGION) )
Building nodeset around goal:  _4:in(_:TidWPjhF65 _4:Texas)
Building inference step for  Proof step for _4:in(_:TidWPjhF65 _4:Texas)
Inferred from <TerminalNode (pass-thru): CommonVariables: [?WHERE] (0 in left, 1 in right memories)> via _4:in(?WHERE _4:Texas) :- _4:home(_4:dan ?WHERE)
Building nodeset around goal (justified by a direct assertion):  _4:home(_4:dan _:TidWPjhF65)
Building nodeset around goal (justified by a direct assertion):  _4:home(_4:dan _:TidWPjhF65)