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: dilemma-program
and classify-program are 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). It needs a
backend to enumerate optima; with none, classify-program reports every contested datum
:supportable, so bravely holds for each and cautiously for none — honest (each is
one of several) and never overclaiming forced.
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: `dilemma-program` and `classify-program` are 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). It needs a backend to enumerate optima; with none, `classify-program` reports every contested datum `:supportable`, so `bravely` holds for each and `cautiously` for none — honest (each *is* one of several) and never overclaiming forced. ## 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 |