nemo
nemo copied to clipboard
Question about behavior of existsence operator
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?