vaelii.impl.abduce — com.vaelii/vaelii 0.13.0

What would have to be true.

Backward chaining answers is this provable? Abduction answers the complementary question — what would have to be true for it to be provable? — and mints the answer as a hypothesis: an ordinary premise, in a context of its own, at :default strength, assumed rather than derived.

The hard parts of abduction are containment, arbitration and cleanup, and this engine already had all three, built for other reasons:

• Containment is the context lattice. A hypothesis goes into a fresh context hung below the asking context, so it sees everything the question could see and nothing that existed before it can see the hypothesis. A shipped rule firing over a hypothesis places its conclusion in that context, because placement is the maximal common descendant (docs/contexts.md) — so the consequences land inside the thing that gets discarded, with nothing arranging for it. That is the sandbox's shape (vaelii.impl.sandbox), for the same reason.
• Arbitration is strengths. A hypothesis is asserted :default, so it is defeasible by construction: a :monotonic fact that contradicts it wins through the ordinary defeat path, with no abduction-specific rule anywhere.
• Cleanup is retraction. A hypothesis is a premise, so retract! and the dependency-directed sweep remove it and everything it supported.

So the new code here is the search — finding the dead end and deciding what may be assumed — and not the belief plumbing.

Two things the caller is owed, and they are the contract:

1. An ignored abduce leaves the KB as it found it. The lifecycle tears the context down before returning unless :keep? says otherwise, and it tears it down on the way out of an exception too.
2. Every answer names its assumptions. Solutions come back beside the hypothesis set that licensed them, never as if they had been proved. An empty :hypotheses is the claim that nothing was assumed.

See docs/abduction.md.

abducible? clj

(abducible? kb sentence context)

May sentence be hypothesized in context? The whole gate, cheapest test first.

• A ground positive literal. An open hypothesis is a skolemization question (docs/skolem.md) and not this one, so an unbound variable refuses rather than enumerates. A negation has functor not, which nothing declares abducible, so the grant below excludes it with no rule of its own.
• Declared abducible, read scoped from context — the one gate that is a grant rather than a veto, and the reason a KB with no abduciblePredicate in it abduces nothing at all.
• Legally assertible: the same four checks every minted sentence passes (special/inadmissible) — naming, the definitional constraints, well-formedness, edge stratification. A sentence assert would refuse must not be one the search assumes, or abduction becomes a way around the checks.
• Not already contradicted where it would be minted.

context-for clj

(context-for token)

The abduction context named by token. CxAbduction<token> satisfies the context naming invariant, so it is an ordinary context in every other respect.

default-opts clj

The caps, and why each exists.

:max-hypotheses bounds how much may be assumed in one call. An uncapped abducer over a rule-rich KB does not terminate usefully — every dead end offers a hypothesis and every hypothesis opens fresh dead ends — so the cap is what makes the loop finite rather than merely usually-finite.

:max-depth bounds where one may be assumed: a dead end reached through more than this many rule expansions is left alone. A hypothesis minted twelve rules deep explains the goal in the sense that anything explains anything.

Both are reported when they bite (:status, :refused), never silently applied.

discard! clj

(discard! kb actx ops)

Discard the abduction context whole: every sentex in it, then the edge that made it a context. Answers {:removed-sentexes n :removed-justifications n}.

One edit for the extent, so it is one settle and the dependency-directed sweep does the rest — a conclusion derived from a hypothesis goes with the hypothesis, and its justification with it. The edge is fetched separately because it was never in the extent: genlCx is forced-decontextualized, so it is stored in CxUniverse.

Idempotent: a context already gone has an empty extent and no edge. Irreversible, hence the ! — that is the whole point of it.

maybe-abduce clj

(maybe-abduce kb goal context {:keys [max-depth]} depth)

The hypothesis this dead end licenses, or nil.

goal is a subgoal the search exhausted, depth the rule expansions taken to reach it. This is the decision function a proof-search hook calls, and everything it needs is in its arguments — which is what lets one rule govern the standalone pass here and any hook inside the search that calls it.

run clj

(run kb goals context opts ops)

Prove goals in context, hypothesizing what the proof needs and cannot find.

ops is the seam — {:rules-fn f :assert f :edit f}, everything abduction needs from the layer above it and does not name (see "the seam" above). goals is the vector form the DFS takes.

Answers

{:solutions   [binding-map …]     under the hypotheses
 :hypotheses  [{:sentence :context :handle} …]
 :refused     [sentence …]        dead ends the gate would not assume
 :context     CxAbductionX
 :status      :complete | :capped}

:hypotheses empty means the goal was proved outright — nothing was assumed, and the solutions are as good as prove's. Otherwise the solutions hold given those sentences, which is why the two travel together.

The loop is: prove, gather dead ends, mint what the gate allows, prove again. Each round mints at least one hypothesis or stops, and the minted set is capped, so there are at most :max-hypotheses rounds. Minting is what makes progress possible — a hypothesis satisfies the antecedent that dead-ended, and the search reaches one rule further, exposing the next thing it lacks.

:refused is reported only when nothing was proved, which is when a caller asks why nothing: a gate that narrows silently reads as "there was nothing to find", when the truth may be that a predicate was never granted. :status :capped is the other half — candidates remained and there was no room for them.

opts takes default-opts' caps plus :keep?. Without it the context is torn down before returning, so an ignored call leaves the KB as it found it; with it the context stands and the caller owns it — inspect the hypotheses, watch one get defeated, commit one by asserting it somewhere that outlives the scratch — and discards it with vaelii.core/abduce-discard!. Committing is deliberately the caller's: abduction proposes.