Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A backward rule nested in the conclusion of a forward rule cause EYE to freeze #32

Closed
blackwint3r opened this issue Jan 28, 2022 · 2 comments

Comments

@blackwint3r
Copy link

blackwint3r commented Jan 28, 2022

It seems that rules of the form like formula1 => {formula2 <= formula3} are not supported by EYE, and cause the reasoner to get stuck, but in some cases this is the only way to achieve my requirement, and I can’t think of a way to work around it.

For example, In the example below, the predicate in the conclusion of a rule is a variable, and the rule also need to be a backward rule itself:

@prefix : <#>.
:know :type :Reflexive.
{:Alice :know :Alice} => {:TEST :PASS 1}.

# {?x ?p ?x} <= {?p :type :Reflexive}.  # doesn't work, not surprising
# {?p :type :Reflexive} =>  {?x ?p ?x}.  # doesn't work either, not surprising
{?p :type :Reflexive} =>  {@forAll :x. {:x ?p :x} <= true }.  # I hope this works

With eye ./test.n3 —nope —pass-only-new what I expected to get:

{ ?x :know  ?x} <= true.   # I expect that `:know` is bound to `?p`  in the nested rule, and produce this rule.
:TEST :PASS 1.

But the actual result is that EYE get stuck.

Another example where nested rules of this form need to be used:

@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .

log:rawType :sub-property-of :type.
{1 type rdfs:Literal } => {:TEST :PASS 2}.

#{?a ?p2 ?b} <= {?a ?p1 ?b. ?p1 :sub-property-of ?p2}.
#{?p1 :sub-property-of ?p2. ?a ?p1 ?b} => {?a ?p2 ?b} .
{?p1 :sub-property-of ?p2 } => {@forAll :a, :b. {:a ?p2 :b} <= {:a ?p1 :b} }.
@josd
Copy link
Collaborator

josd commented Jan 28, 2022

Thanks for discovering and it wasn't easy to solve but it should be fixed in https://github.com/josd/eye/releases/tag/v22.0128.1551
The first test now gives

?U_0 :know ?U_0.
:TEST :PASS 1 .

and the second test (after correcting test to :test in line 5) now gives

{?U_0 <file:///tmp/test2.n3#type> ?U_1} <= {?U_0 log:rawType ?U_1}.
<file:///tmp/test2.n3#TEST> <file:///tmp/test2.n3#PASS> 2 .

@blackwint3r
Copy link
Author

I'm also guessing this might be hard to solve,didn't expect fixed so soon. Really appreciate your work !

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants