eyereasoner / eye

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

Unexpected behaviour from backward chaining rules, for blank nodes and query variables #116

Open renyuneyun opened 2 weeks ago

renyuneyun commented 2 weeks ago

Observation 1

Backward chaining rules whose conclusion contains new query variables (that do not exist in premise) result in reasoner error: ** ERROR ** gre ** error(permission_error(modify,static_procedure,(,)/2),context(system:assertz/1,_210)).

Example:

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

:Alice a :Human.

{
    ?m a :World;
        :has ?h.
} <= {
    ?h a :Human.
}.

Observation 2

Backward chaining rules whose conclusion contains blank nodes seems to do nothing.

Example:

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

:Alice a :Human.

{
    _:m :has ?h.
} <= {
    ?h a :Human.
}.

{ 
    ?a :has ?b.
} => {
    ?a :has ?b.
}.

The example in #35 also does not work.

josd commented 2 weeks ago

For Observation 1: the conclusion must be a single triple.

For Observation 2: put

{ 
    ?a :has ?b.
} => {
    ?a :has ?b.
}.

in a separate query file or use

{ 
    ?a :has ?b.
} =^ {
    ?a :has ?b.
}.

where =^ is syntactic sugar for log:query.

renyuneyun commented 1 week ago

Thanks for the info! In particular, for observation 2, thanks for hinting again -- I forgot it was expected to be a different one now.

For observation 1: It's good to have this documented explicitly, as it's not described anywhere. In particular, N3 language spec did not say anything about a difference in the number of triples for backward chaining rules and forward chaining rules.

A related question: is there a way to do something close to multiple-triples-in-backward-chaining? What I need is to circumvent a rule to be fired all the time, but only when needed from some other rules. This is because the rule would be too general on its own, and thus resulting in too many unneeded triples if not only fired in a few cases (the "other rules").

josd commented 1 week ago

A related question: is there a way to do something close to multiple-triples-in-backward-chaining? What I need is to circumvent a rule to be fired all the time, but only when needed from some other rules. This is because the rule would be too general on its own, and thus resulting in too many unneeded triples if not only fired in a few cases (the "other rules").

You can rewrite them as multiple backward rules, that is

C1 AND C2 AND C3 <= P.

can be rewritten as

C1 <= P.
C2 <= P.
C3 <= P.

just make sure to add log:skolem functions in P.

So your example

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

:Alice a :Human.

{
    ?m a :World;
        :has ?h.
} <= {
    ?h a :Human.
}.

could be rewritten as

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://example.org/ns/>.

:Alice a :Human.

{
    ?m a :World.
} <= {
    ?h a :Human.
    (?h) log:skolem ?m.
}.
{
    ?m :has ?h.
} <= {
    ?h a :Human.
    (?h) log:skolem ?m.
}.

# queries
{
    ?S a ?O.
} =^ {
    ?S a ?O.
}.

{
    ?S :has ?O.
} =^ {
    ?S :has ?O.
}.

and so we get

$ eye --quiet --nope rui3.n3
@prefix : <http://example.org/ns/>.
@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/9770c5da-4cf9-4896-be29-0e498895034b#>.

:Alice a :Human.
skolem:t_0 a :World.
skolem:t_0 :has :Alice.
renyuneyun commented 1 week ago

Thanks for the tip! It seems to be working. (But for my real code, the result is now incorrect. I'll investigate that.)

However, a seeming consequence is: some other (but not all?) unnamed nodes are also assigned a skolem:... ID, and becomes named nodes. Is this expected? Is there a way to prevent this behaviour? (I'm using eye v10.19.6.)

josd commented 1 week ago

Could you give a concrete example where you get unexpected skolem IRIs?