Built-ins can’t use e:Scope parameter to refer to other n3 files.

[blackwint3r]

Here is my test case:

$ cat test-a.n3
PREFIX : <http://www.example.com/test#> 
PREFIX e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>
:a :b :c.
{((<>) 1) e:call {:a :b :c} } => {:TEST :PASS 1}. 
{((<./test-b.n3> ) 1) e:call {:a :b :c} } => {:TEST :PASS 2}. #don’t  work
{((<> <./test-b.n3> ) 1) e:call {:a :b :c} } => {:TEST :PASS 3}. #don’t  work

$cat test-b.n3
PREFIX : <http://www.example.com/test#> 
:a :b :c.

$ eye --pass-only-new --nope ./test-a.n3
:TEST :PASS 1 .

I also tried other build-ins with e:Scope parameter, such as e:findall, and got similar result. Is this a bug?

[josd]

It is not a bug, it is not supported.

Like said in the schema http://eulersharp.sourceforge.net/2003/03swap/log-rules.html#Scope the scope is a (context recursion) pair where a context is a list of consulted URI's and a recursion is the deductive closure recursion number. The consulted URI's are the <data>* ones that you give in the command line eye <options>* <data>* <query>*

[blackwint3r]

Thank you for your explanation, but I am still confused. With same n3 files above, Use the following command line: $ eye --nope ./test-a.n3 ./test-b.n3 --pass-only-new

I get :TEST :PASS 3 .

It seems that in order for e:call to succeed, the consulted URI's in the scope must be exactly the same as<data>* ones in the command line I gave, and cannot be part of it. Is e:Scopedesigned to work like this?

But what I want to do is to check if the target formula can succeed in another given formula or a given .n3 file.

so I wish to have:

:TEST :PASS 1 .
:TEST :PASS 2 .
:TEST :PASS 3 .

How can I achieve this?

[josd]

It seems that in order for e:call to succeed, the consulted URI's in the scope must be exactly the same as<data>* ones in the command line I gave, and cannot be part of it. Is e:Scopedesigned to work like this?

Exactly and its typical use is as a variable which will get bound to the reasoning scope to be shown in proofs.

so I wish to have:

:TEST :PASS 1 .
:TEST :PASS 2 .
:TEST :PASS 3 .

How can I achieve this?

This not possible with e:call but you could for instance use

PREFIX log: <http://www.w3.org/2000/10/swap/log#>
PREFIX : <http://www.example.com/test#> 

:a :b :c.
{<./test-a.n3>!log:semantics log:includes {:a :b :c} } => {:TEST :PASS 1}. 
{<./test-b.n3>!log:semantics log:includes {:a :b :c} } => {:TEST :PASS 2}.
{(<./test-a.n3>!log:semantics <./test-b.n3>!log:semantics)!log:conjunction log:includes {:a :b :c} } => {:TEST :PASS 3}.

[blackwint3r]

Thank you for your reminder, but there is a important semantic difference compared to what I want to achieve , that is this usage do not support the conclusion of backward rule, and e:call seems the only way to do this. For example:

PREFIX log: <http://www.w3.org/2000/10/swap/log#>
PREFIX : <http://www.example.com/test#>
PREFIX e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>

{:d :e :f} <= {:a :b :c}.
:a :b :c.
{<>!log:semantics log:includes {:d :e :f} } => {:TEST :PASS 1}.#did not pass
{((<>) 1) e:closure {:d :e :f} } => {:TEST :PASS 2}. #did not pass
{((<>) 1) e:call {:d :e :f} } => {:TEST :PASS 3}. #passed

log:conclusion do not satisfied for same reason. (I had also struggled to construct a backward compatible version of log:conclusion but failed. Something like {?f e:callInFormula ?g} <= {?f e:convertToString ?s. ?s e:saveToTmpFile ?path. ((?path) 1) e:call ?g } . ).

[josd]

The latest version of EYE https://github.com/josd/eye/releases/tag/v22.0103.1833 is extending e:call so that is able to call the object formula in the subject formula.

So now it can can do the job:

$ cat test-a.n3
PREFIX : <http://www.example.com/test#>

{:d :e :f} <= {:a :b :c}.
:a :b :c.

$ cat test-c.n3
PREFIX log: <http://www.w3.org/2000/10/swap/log#>
PREFIX e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>
PREFIX : <http://www.example.com/test#>

{<./test-a.n3>!log:semantics e:call {:d :e :f} } => {:TEST :PASS 1}.

$ eye --quiet --nope test-c.n3 --pass-only-new 2>/dev/null
PREFIX log: <http://www.w3.org/2000/10/swap/log#>
PREFIX e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>
PREFIX : <http://www.example.com/test#>

:TEST :PASS 1 .

Putting test-c.n3 into test-a.n3 and running test-a.n3 is an infinite loop.

[blackwint3r]

This is really great! Now I can check a target formula both in a file and in a formula. Thank you for your prompt reply and hard work!