eyereasoner / eye

Euler Yet another proof Engine
https://eyereasoner.github.io/eye/
MIT License
124 stars 17 forks source link

Missing examples and/or specification of `--query` #111

Closed renyuneyun closed 2 months ago

renyuneyun commented 2 months ago

I'm trying to write some tests for my logical program, and thus thought about using --query to form some unit tests.

I'm aware of --entail, but it alone is not enough because the deductive closure contains a lot more triples, which I hope to be managed into different chunks of tests. I need to a) test equivalence between real output and expected output, and b) find out what is different. Not sure about the best way. Any pointers to that affair is appreciated as well.

However, I found the document for --query <n3-query> is extremely limited, and it's not obvious what spec the <n3-query> follows. Based on the name and description (of the parameter), it should be a n3 document, which represents some query. However, I could not find the word query for this purpose in n3 spec -- it only says what is a query in n3 rules, but query is not a standalone construct for n3 outside of rules.

So, what is the expected syntax and semantics for the <n3-query>?

What I tried: I tried to find some examples in the repo, but saw different things by searching query (esp, as file name). The commonality is that all uses n3 rules with query in premise. However, some of them repeat the (syntactically) same premise and conclusion; some have different premise and conclusion; some uses backward chaining while most uses forward chaining. And in my tests, the results are not always as expected if I simply consider premise to be the input filter and conclusion to be the output filter.

josd commented 2 months ago

--query is that same as Cwm's --filter= which is nicely explained at https://www.w3.org/2000/10/swap/doc/Processing#Filtering So it is typically a forward rule but the conclusions are not added to the deductive closure but directed to the reasoner output. In eye you can also use <= but is rarely used for queries. We recently also added an experimental log:query to have query rules amongst other rules and it also has =^ as syntactic sugar.

renyuneyun commented 2 months ago

Thanks for the info. That indeed answered my main questions.

However, I encounter an unexpected behaviour during my tests.

I have an n3 file with the following content:

@prefix : <http://example.org/>.

:Alice :hasFriend :Bob.
:Alice a :Human, :Being.

{ ?A a :Human. } => {
    ?A :has [ a :Leg ].
}.

And then a query file with the following content:

@prefix : <http://example.org/>.

{
    ?A a :Human.
    ?A ?p ?o.
} => {
    ?A ?p ?o.
}.

{
    ?A a :Human; :has [?p ?o].
} => {
    ?A a :Human; :has [?p ?o].
}.

I would expect the query result to be :Alice with all relevant properties, and with one :has [ a :Leg ]. However, the actual result is:

:Alice :hasFriend :Bob.
:Alice a :Human.
:Alice a :Being.
:Alice :has _:sk_0.
:Alice :has _:sk_1.
_:sk_1 a :Leg.

It has a strange additional _:sk_0 node, without any properties. If I also have :Bob a :Human, it will also have this additional node. This won't happen if :Alice :has [ a :Leg ]. is asserted rather than inferred.

josd commented 2 months ago

Right and we are currently moving towards

⚠️ variables

and so

@prefix : <http://example.org/>.

:Alice :hasFriend :Bob.
:Alice a :Human, :Being.

{ ?A a :Human. } => {
        ?A :has ?B.
        ?B a :Leg .
}.

with query

@prefix : <http://example.org/>.

{
        ?A a :Human.
        ?A ?p ?o.
} => {
        ?A ?p ?o.
}.

{
        ?A a :Human; :has ?s.
        ?s ?p ?o.
} => {
        ?A a :Human; :has ?s.
        ?s ?p ?o.
}.

gives

@prefix : <http://example.org/>.

:Alice :hasFriend :Bob.
:Alice a :Human.
:Alice a :Being.
:Alice :has _:sk_0.
_:sk_0 a :Leg.
renyuneyun commented 2 months ago

Thanks for the reply. I might be missing some information, and don't understand why SAGE and the three rules of variables is relevant to the issue?

My only possible guess is: because I used shorthand syntax for an unlabelled node, it is not interpreted as a variable in query, but rather an assertion somehow? (And the assertion, because its content is [ ?p ?o ] (i.e., _:b0 ?p ?o.), it is not any concrete triple, and thus ignored?)

(It seems changing the original n3 file to explicit variable ?B is unnecessary, right?)

josd commented 2 months ago

Right, forget about SAGE ;-)