nemo icon indicating copy to clipboard operation
nemo copied to clipboard

Question about behavior of existsence operator

Open StarGazerM opened this issue 7 months ago • 2 comments

According to document ! with unbound meta var name can be used to create a placeholder, but seems following code, can't create any placehold? By definition this should be an infinity loop to show the continuous of foo?

foo(1).
foo(!y) :- foo(?x).

@export  foo :- csv {}.

And I also tried

foo(1).
foo(!y), bar(!y) :- foo(?x).

@export  foo :- csv {}.
@export  bar :- csv {}.

I this test example, a empty placeholder is generated for both foo and bar, but seems never used to inference another? I also check existence op paper https://iccl.inf.tu-dresden.de/w/images/f/f6/An_Existential_Rule_Framework_for_Computing_Why_Provenance_On_Demand_for_Datalog_%282%29.pdf

In the paper, existence operator is suppose to wit why provenance, which is a invariant tracks where each tuple comes could possibly comes from, so each of these place holder should be able to map to root node of an concrete proof tree. Does nemo's existence operator the same thing as whats in why-provenance-on-demand paper?

StarGazerM avatar Jul 17 '24 00:07 StarGazerM