ShotTx.Proof.Step (ShotTx v0.0.1)

A single node in a ShotTx.Proof derivation tree.

label — the derivation's line number in textbook style;
```
         unique within a proof.
```
formula — the derived (or :given) formula, as a term id.

rule — atom symbol of the applied tableau rule

         (`:alpha`, `:beta`, `:gamma`, …), or `nil` for `:given`
         and `:closure` nodes.

sources — labels of premise steps this step was derived from.

kind — one of :given (initial formula), :rule

         (derived), `:closure` (branch-closing ⊥ leaf),
         or `:model` (countermodel witness leaf).

children — subordinate steps (siblings under a β-split share
```
         the same parent).
```
model — {atoms, defs} when kind == :model, otherwise nil.

Summary

Types

kind()

t()

Types

kind()

@type kind() :: :given | :rule | :closure

t()

@type t() :: %ShotTx.Proof.Step{
  children: [t()],
  formula: ShotDs.Data.Term.term_id() | nil,
  kind: kind(),
  label: pos_integer(),
  model: term(),
  rule: atom() | nil,
  sources: [pos_integer()]
}