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 presence check (nat-read/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 presence check (`nat-read/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 raw witnesses)Mint the skolem constant of each of witnesses (witnesses above) and return the
rule's substituted conclusion raw with each variable replaced by its constant.
Mint the skolem constant of each of `witnesses` (`witnesses` above) and return the rule's substituted conclusion `raw` with each variable replaced by its constant.
(witnesses rule bindings free)[[var expr]…], free sorted: the NAT (SkolemFn <rule-digest> i <frontier-values…>)
the i-th still-unbound (existential) variable of a rule's conclusion names under
bindings, before anything is minted.
`[[var expr]…]`, `free` sorted: the NAT `(SkolemFn <rule-digest> i <frontier-values…>)` the i-th still-unbound (existential) variable of a rule's conclusion names under `bindings`, before anything is minted.
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 |