23 lines
684 B
Plaintext
23 lines
684 B
Plaintext
|
# Skolem chase: deterministic labeled nulls for existential variables.
|
||
|
|
#
|
||
|
|
# With the Skolem variant, re-applying a rule with the same frontier
|
||
|
|
# bindings reuses the same null value, so the chase terminates even for
|
||
|
|
# rules that introduce existentials. Compare this with the oblivious
|
||
|
|
# variant, which generates a fresh null each round and hits the step
|
||
|
|
# limit.
|
||
|
|
#
|
||
|
|
# NOTE: the REPL uses the restricted chase by default. To run with the
|
||
|
|
# Skolem variant, use the Rust API:
|
||
|
|
#
|
||
|
|
# let result = skolem_chase(instance, &rules);
|
||
|
|
|
||
|
|
fact Person(alice).
|
||
|
|
fact Person(bob).
|
||
|
|
fact Person(carol).
|
||
|
|
|
||
|
|
# Every person has an id (existential Y).
|
||
|
|
rule Person(?X) -> HasId(?X, ?Y).
|
||
|
|
|
||
|
|
run.
|
||
|
|
query HasId(?X, ?Y)?
|