Head existentials: the deterministic SkolemFn witness a rule head (exists ?y C)
fires to, reified through vaelii.impl.nat. Called from two layers: the assert path
declares SkolemFn when it stores such a rule, and the forward chainer mints at each
firing. See docs/skolem.md.
Head existentials: the deterministic `SkolemFn` witness a rule head `(exists ?y C)` fires to, reified through `vaelii.impl.nat`. Called from two layers: the assert path declares `SkolemFn` when it stores such a rule, and the forward chainer mints at each firing. See docs/skolem.md.
(ensure-skolem-function kb)Declare SkolemFn a reifiable_function if it is not already, which also turns on
the NAT orphan-cleanup gate (nat/any-reifiable-functions?). Idempotent; asserted
without chaining.
Declare `SkolemFn` a `reifiable_function` if it is not already, which also turns on the NAT orphan-cleanup gate (`nat/any-reifiable-functions?`). Idempotent; asserted without chaining.
(has-existential-head? sentence)Does sentence assert a rule whose consequent is a head existential (exists ?y C)?
Read past any set/*Rule / exceptWhen wrapper.
Does `sentence` assert a rule whose consequent is a head existential `(exists ?y C)`? Read past any `set/*Rule` / `exceptWhen` wrapper.
The reifiable function every skolem constant is an application of.
The reifiable function every skolem constant is an application of.
(skolemize-conclusion kb rule raw bindings free)Replace each still-unbound (existential) variable free in a rule's substituted
conclusion raw with its skolem constant, the NAT (SkolemFn <rule-digest> i <frontier-values…>) for the i-th of free sorted, and return the ground conclusion.
Replace each still-unbound (existential) variable `free` in a rule's substituted conclusion `raw` with its skolem constant, the NAT `(SkolemFn <rule-digest> i <frontier-values…>)` for the i-th of `free` sorted, and return the ground conclusion.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |