ShotTx.Proof (ShotTx v0.0.1)

A tableau derivation reconstructed from the closed-branch traces returned by the prover.

The proof is a tree of Step nodes. Each step carries a unique integer label — the line number you would write in a textbook derivation — and a sources field listing the labels of the steps it was derived from. Branching rules (β, instantiate) produce multiple sibling steps that all cite the same source; they are not represented as a separate node above their alternatives.

Step kinds

:given — an initial formula (an assumption or the negated
```
         conclusion). No rule, no sources.
```

:rule — a formula derived by applying a rule to one earlier

         step. `sources` is the singleton list of that premise's
         label, `rule` the symbol of the applied rule
         (`:alpha`, `:beta`, `:gamma`, …).

:closure — the ⊥ leaf that closes a branch. sources cites the

         contradictory pair (or the `false` / `¬true` literal
         for trivial closures).

Construction

from_refutation/4 linearises each closed branch's trace into a flat list of "events" — one event per produced formula — and groups branches whose first events agree under a single Step, recursing into the divergent tails. Branches share Steps as long as they share prefixes; the moment they pop different rules from their queues, two sibling Steps emit and the tree forks. This is why a β-step ends up with two siblings (one per disjunct) and pure-trunk α/γ chains stay linear.

Branch ids encode the path through every β/instantiate split as _A / _B / _I{idx} segments; the linearisation consumes one segment per branching event to pick the correct side.

Renders to Mermaid via to_mermaid/1 and to a plain-text tableau layout via to_text/1.

Summary

Types

t()

Functions

auto_aliases(proof)

Walks the proof and produces an alias map giving each fresh reference a short readable name

from_countermodel(closed_traces, initial_formulas, model_branch_id, model_trace, arg)

from_partial(branch_traces, initial_formulas)

Build a partial Proof from whatever traces happen to be in the trace store at a checkpoint (e.g. on timeout).

from_refutation(branch_traces, initial_formulas, substitution, flex_pairs)

Build a Proof from the per-branch traces returned by the prover.

latex_aliases(proof)

Like auto_aliases/1 but emits raw LaTeX names (\alpha, X, c, …). Used by to_mermaid/2 via LatexFormatter.with_latex_aliases/2 so fresh metas render as proper math identifiers instead of the default V_{short_ref} fallback.

to_mermaid(proof, opts \\ [])

Render the proof tree as a Mermaid graph TD diagram with LaTeX formula labels (rendered via KaTeX in Livebook / Mermaid).

to_text(proof, opts \\ [])

Render the proof tree as a plain-text tableau derivation.

Types

t()

@type t() :: %ShotTx.Proof{
  flex_pairs: list(),
  root: ShotTx.Proof.Step.t() | nil,
  substitution: map()
}

Functions

auto_aliases(proof)

@spec auto_aliases(t()) :: %{required(reference()) => String.t()}

Walks the proof and produces an alias map giving each fresh reference a short readable name:

type-variable refs → α, β, γ, ... (then α4, α5, ...)
free-variable refs (γ/π) → X, Y, Z, ... (then X4, X5, ...)
constant refs (skolems) → c, d, e, ... (then c4, c5, ...)

from_countermodel(closed_traces, initial_formulas, model_branch_id, model_trace, arg)

@spec from_countermodel(
  map(),
  [ShotDs.Data.Term.term_id()],
  String.t(),
  list(),
  {[ShotDs.Data.Term.term_id()], map()}
) :: t()

from_partial(branch_traces, initial_formulas)

@spec from_partial(map(), [ShotDs.Data.Term.term_id()]) :: t()

Build a partial Proof from whatever traces happen to be in the trace store at a checkpoint (e.g. on timeout).

Closed branches keep their ⊥ leaf; open / in-flight branches simply end at their last recorded step. No global substitution or flex constraints are attached.

from_refutation(branch_traces, initial_formulas, substitution, flex_pairs)

@spec from_refutation(map(), [ShotDs.Data.Term.term_id()], map(), list()) :: t()

Build a Proof from the per-branch traces returned by the prover.

branch_traces — %{branch_id => trace}, oldest entry first per trace. Each trace entry is {source, classified_rule, [produced]}.
initial_formulas — the seeds of the root branch (assumptions plus the negated conclusion); they become the :given steps.
substitution, flex_pairs — refutation metadata, threaded through for use by callers that want to display the global witness.

latex_aliases(proof)

@spec latex_aliases(t()) :: %{required(reference()) => String.t()}

to_mermaid(proof, opts \\ [])

@spec to_mermaid(
  t(),
  keyword()
) :: String.t()

Render the proof tree as a Mermaid graph TD diagram with LaTeX formula labels (rendered via KaTeX in Livebook / Mermaid).

Branch points (β / instantiate) emit solid arrows; linear derivations emit dotted arrows. Each rule node carries its label, the derived formula and a justification footer naming the rule symbol and the cited line(s).

to_text(proof, opts \\ [])

Render the proof tree as a plain-text tableau derivation.

Linear chains print one step per line at the current indentation level. At a branch point the children expand under tree connectors ├── and └──; descendant lines carry │ continuation markers as long as there are siblings still to be rendered.

Example output:

1. (p ∨ q)            [given]
2. ¬p                 [given]
3. ¬q                 [given]
├── 4. p              [β on 1]
│   5. ⊥              [2, 4]
└── 6. q              [β on 1]
    7. ⊥              [3, 6]