A query-time prover for (bravely S) and (cautiously S) — brave/cautious reading
of the dilemmas the KB currently holds, answered as a read and never committed.
(cautiously S) holds when S is in every optimal labeling of the current
dilemmas; (bravely S) when S is in some. Over a coexisting P/¬P dilemma the
engine declines to arbitrate (docs/exceptions.md), both sides are IN, and an ordinary
ask reports both — so it cannot tell the forced belief from the arbitrary one. A
brave/cautious read can: in a Nixon diamond (bravely (pacifist N)) holds and
(cautiously (pacifist N)) does not, because the other labeling gives it up.
This is the read-path delivery of the forced/arbitrary signal. The only prior route to
it, do/labeling, commits — it re-asserts the kept side at :monotonic and defeats
the loser everywhere (docs/labeling.md). This prover commits nothing: it reads
label/classify-dilemmas — dilemma-program/classify-program with a backend, the
solve-free label/classify-local without one — all pure reads over settled belief, so a
query answers and leaves belief, contradictions and last-program exactly as they were.
Registered like the other optional reasoners — (add-reasoner kb :brave-cautious) — so
the ASP stack stays off a KB's load path until a caller asks (docs/asp.md). With a
backend it enumerates optima and classifies exactly; with none it reads the solve-free
JTMS bracket (label/classify-local), which enumerates the dilemmas' optimal
resolutions from the dependency graph and classifies each datum by which resolutions keep
it — :true in every, :supportable in some, :false in none. Exact for a datum whose
clusters it enumerates: the one cluster its support touches, or several whose product of
resolutions stays within VAELII_CLASSIFY_MAX_JOINT_OPTIMA. A datum past that cap, or
one touching a cluster too large to enumerate, degrades to :supportable
(docs/labeling.md).
Ground S only. (bravely (pacifist N)) is answered; an open (bravely (pacifist ?x)) is not applicable and no prover answers it, rather than enumerating the contested
atoms — the same restraint different takes.
A query, not a fact and not an antecedent. bravely/cautiously are not
assertible (wff/brave-cautious-problems): a stored one would be a computed value with
no way to keep it current, the reason the aggregates and unknown are refused too. As a
rule antecedent the answer carries no support (it is not a SupportingProver), so the
forward join drops it and it derives nothing — a read, not something belief rests on.
Threading its support (the dilemma's contested handles) so a rule could rest on it is the
open design point, deferred until a use asks for it.
A query-time prover for `(bravely S)` and `(cautiously S)` — brave/cautious reading of the dilemmas the KB currently holds, answered as a read and never committed. ## What it answers `(cautiously S)` holds when `S` is in **every** optimal labeling of the current dilemmas; `(bravely S)` when `S` is in **some**. Over a coexisting `P`/`¬P` dilemma the engine declines to arbitrate (docs/exceptions.md), both sides are IN, and an ordinary `ask` reports both — so it cannot tell the *forced* belief from the *arbitrary* one. A brave/cautious read can: in a Nixon diamond `(bravely (pacifist N))` holds and `(cautiously (pacifist N))` does not, because the other labeling gives it up. This is the read-path delivery of the forced/arbitrary signal. The only prior route to it, `do/labeling`, **commits** — it re-asserts the kept side at `:monotonic` and defeats the loser everywhere (docs/labeling.md). This prover commits nothing: it reads `label/classify-dilemmas` — `dilemma-program`/`classify-program` with a backend, the solve-free `label/classify-local` without one — all pure reads over settled belief, so a query answers and leaves belief, `contradictions` and `last-program` exactly as they were. ## Opting in Registered like the other optional reasoners — `(add-reasoner kb :brave-cautious)` — so the ASP stack stays off a KB's load path until a caller asks (docs/asp.md). With a backend it enumerates optima and classifies exactly; **with none it reads the solve-free JTMS bracket** (`label/classify-local`), which enumerates the dilemmas' optimal resolutions from the dependency graph and classifies each datum by which resolutions keep it — `:true` in every, `:supportable` in some, `:false` in none. Exact for a datum whose clusters it enumerates: the one cluster its support touches, or several whose product of resolutions stays within `VAELII_CLASSIFY_MAX_JOINT_OPTIMA`. A datum past that cap, or one touching a cluster too large to enumerate, degrades to `:supportable` (docs/labeling.md). ## Where it stops **Ground `S` only.** `(bravely (pacifist N))` is answered; an open `(bravely (pacifist ?x))` is not applicable and no prover answers it, rather than enumerating the contested atoms — the same restraint `different` takes. **A query, not a fact and not an antecedent.** `bravely`/`cautiously` are not assertible (`wff/brave-cautious-problems`): a stored one would be a computed value with no way to keep it current, the reason the aggregates and `unknown` are refused too. As a rule antecedent the answer carries no support (it is not a `SupportingProver`), so the forward join drops it and it derives nothing — a read, not something belief rests on. Threading its support (the dilemma's contested handles) so a rule could rest on it is the open design point, deferred until a use asks for it.
(brave-cautious-prover)The (bravely S) / (cautiously S) prover, for add-prover — or, the ordinary way in,
(add-reasoner kb :brave-cautious).
The `(bravely S)` / `(cautiously S)` prover, for `add-prover` — or, the ordinary way in, `(add-reasoner kb :brave-cautious)`.
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 |