Some built-in predicates such as `log:conclusion` transform backward rules into forward during output binding #134

blackwint3r · 2025-02-08T10:02:25Z

Let me explain what I want to do: I want to perform reasoning inside a graph, also called inline inference. Specifically, I want to create a predicate similar to eye —pass-only-new command, receive a graph as subject, and outputs (binding to object) only the new conclusions asserted after reasoning within the graph.

Here's my first try:

@prefix math: <http://www.w3.org/2000/10/swap/math#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <#>.

{?g :conclusionOnlyNew ?g3} <= {
    ?g log:conclusion ?g2.  #using log:inferences instead gives me same result
    (?g2 ?g) e:graphDifference ?g3  # remove original graph contents
    }.

:mykb rdf:value {
    :Socrates a :Human. 
    {?x a :Human} => {?x a :Mortal}. 
    {:Socrates a :Mortal} => {:test1 a :succeed}.

    {?x a :PostiveNum} <= {?x math:greaterThan 0} .
    {123 a :PostiveNum} => {:test2 a :succeed}. 
}.

{:mykb!rdf:value :conclusionOnlyNew ?g} => {:newConclusion :is ?g}. #  reasoning inside the graph

The expected output is:

:newConclusion :is {
    : Socrates a :Mortal.
    :test1 a :succeed.
    :test2 a :succeed.
}

The actual output is:

:newConclusion :is {
    :Socrates a :Mortal.
    :test1 a :succeed.
    :test2 a :succeed.
    true => {
        :Socrates a :Human.
    }.
    {
        ?U_1 math:greaterThan 0.
    } => {
        ?U_1 a :PostiveNum.
    }.
    true => {
        :Socrates a :Mortal.
    }.
    true => {
        :test1 a :succeed.
    }.
    true => {
        :test2 a :succeed.
    }.
}.

Besides the strange sentences of the form true => {...}, there is also { ?U_1 math:greaterThan 0. } => { ?U_1 a :PostiveNum. }, which is outside of my expectation .

So, I did some test, and found that log:conclusion and log:inference incorrectly convert backward rules into forward form in their output (i.e., the bound object ), which causes subsequent processing issues. Nevertheless, they somehow correctly executed the logic of the backward rule, producing :test2 a :succeed.

Namely:

{:mykb!rdf:value log:conclusion ?g} => {:Conclusion :is ?g}.

in my context would yield:

:Conclusion :is {
    :Socrates a :Human.
    :Socrates a :Mortal.
    :test1 a :succeed.
    :test2 a :succeed.
    {
        ?U_2 a :Human.
    } => {
        ?U_2 a :Mortal.
    }.
    {
        :Socrates a :Mortal.
    } => {
        :test1 a :succeed.
    }.
    {
        123 a :PostiveNum.
    } => {
        :test2 a :succeed.
    }.
    true => {
        :Socrates a :Human.
    }.
    {
        ?U_3 math:greaterThan 0.   # backward rule turned into a forward form
    } => {
        ?U_3 a :PostiveNum.
    }.
    true => {
        :Socrates a :Mortal.
    }.
    true => {
        :test1 a :succeed.
    }.
    true => {
        :test2 a :succeed.
    }.
}.

I also attempted to remove sentences of the form true => {...}, leading to my second version:

{?g :conclusionOnlyNew ?g4 } <= {
    ?g log:conclusion ?g2. 
    ?g2 e:findall ({true => ?sth } {true => ?sth} ?list).  #remove sentences of the form `true => {...}`
    #”list" log:trace ?list.
    ?list log:conjunction ?g3.
    (?g2 ?g3) e:graphDifference ?g4.
    }.

# Other parts remain unchanged

But this does not work because elements in ?list are appears in the form ?sth <= true, rather than the expected true => ?sth. This is another bug.

Through some experiments, I have found that many built-in predicates have similar problems with backward rules:

log:semantics, when reading other files, transforms backward rules into forward ones. Interestingly, this does not happen when it reads itself (<> log:semantics ?x).
log:parsedAsN3 has the same issue.
e:findall, as mentioned above, turned forward rules of only the form true => {:s :p :o} into backward. Compared to the previous problem this is a minor issue.

On the other hand, log:includeand e:graphMember able to distinguish between forward and backward rules correctly (even syntactically incorrect forms like :g1 => :g2 and :g1 <= true), seems treating them as ordinary triples, which is my expectation. Here is a simple example:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix : <#>.

:mygraph rdf:value {{:d :e :f} <= {:a :b :c}}.
{:mygraph rdf:value ?g. ?g log:includes {{:d :e :f} ?p ?o} } => {:result :is ?p}.

output:

:result :is log:isImpliedBy.

The text was updated successfully, but these errors were encountered:

josd · 2025-02-08T11:16:45Z

Logically speaking there is nothing broken when converting a backward rule into a forward rule, but it is indeed messy.

For the moment I have simplified log:conclusion to behave as --pass and now with v11.5.9 your original case is giving

:newConclusion :is {
    :Socrates a :Mortal.
    :test1 a :succeed.
    :test2 a :succeed.
}.

blackwint3r · 2025-02-09T12:15:55Z

Thank you for your effort!

And can the log:semantics or log:content and log:parsedAsN3 be fixed? It would be very useful in many scenarios.

An interesting use case: I managed to implement the operation of importing other files in N3:

import_demo1.n3

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

{?scope :imports ?file. ?file log:semantics ?s} => ?s.
#{?scope :imports ?file. ?file log:content ?f. ?f log:parsedAsN3 ?s} => ?s. # Equivalent implementation

[] :imports <./import_demo2.n3>.

{:d :e :f} => {:test1 a :Succeed}.
{123 a :PostiveNum} => {:test2 a :succeed}.

import_demo2.n3

@prefix : <http://www.example.com/ns#>.

# Imports can be recursive
# There is no need to define imports in this file, as long as there are import definitions in the files that import this file!
[] :imports <./import_demo3.n3>.

:a :b :c.

import_demo3.n3

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

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

{?x a :PostiveNum} <= {?x math:greaterThan 0}.

Place these three files in the same directory, then executing eye —pass-only-new import_demo1.n3 should show all tests succeeding. Currently, due to limitations in the implementation of log:semantics, log:content, and log:parsedAsN3, the output does not include :test2 a :succeed.

This is just one example, but implementing this would be useful in many places.

josd · 2025-02-09T13:03:34Z

Should be fixed and now we get

$ eye --version
EYE v11.6.0 (2025-02-09)

$ eye --quiet import_demo1.n3 --pass-only-new
@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/3145cba6-cba4-4fc0-868c-5fe0c7ee1b66#>.
@prefix : <http://www.example.com/ns#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.


skolem:bn_2 :imports <file:///tmp/import_demo3.n3>.
:a :b :c.
{
    :a :b :c.
} => {
    :d :e :f.
}.

{
    ?U_1 a :PostiveNum.
} <= {
    ?U_1 math:greaterThan 0.
}.
:test2 a :succeed.
:d :e :f.
:test1 a :Succeed.

blackwint3r · 2025-02-09T18:42:04Z

Appreciate your help in solving this!

blackwint3r · 2025-02-19T15:22:20Z

I found In the newest version (v11.7.5), the output of my first test case has changed again:

:newConclusion :is {:Socrates a :Mortal. :test1 a :succeed. :test2 a :succeed. true => {:Socrates a :Human}. {?U_1 math:greaterThan 0} => {?U_1 a :PostiveNum}. true => {:Socrates a :Mortal}. true => {:test1 a :succeed}. true => {:test2 a :succeed}}.

The output of second test case (import_demo1/2/3.n3) has also changed back.

Reinstalling version 11.6.0 find it works fine, not sure which update in between broke this fix.

And I also noticed although v11.6.3 made log:conclusion behave as --pass-all, correctly output all forward and backward rules, it also reintroduces weird statements in the form of sth <= true. In my first example above, eye v11.6.3 produce:

:newConclusion :is {:Socrates a :Mortal. :test1 a :succeed. :test2 a :succeed. {:Socrates a :Human} <= true. {:Socrates a :Mortal} <= true. {:test1 a :succeed} <= true. {:test2 a :succeed} <= true}.

josd added a commit that referenced this issue Feb 8, 2025

fixing #134

b7f5acd

josd added a commit that referenced this issue Feb 9, 2025

fixing issue #134

80ba341

blackwint3r closed this as completed Feb 9, 2025

blackwint3r reopened this Feb 19, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Some built-in predicates such as `log:conclusion` transform backward rules into forward during output binding #134

Some built-in predicates such as `log:conclusion` transform backward rules into forward during output binding #134

Some built-in predicates such as log:conclusion transform backward rules into forward during output binding #134

Some built-in predicates such as log:conclusion transform backward rules into forward during output binding #134

Comments

Some built-in predicates such as `log:conclusion` transform backward rules into forward during output binding #134

Some built-in predicates such as `log:conclusion` transform backward rules into forward during output binding #134