# ShotTx v0.0.1 - Table of Contents

> Tableau component of Shot, a parallel Church Simple Type Theory theorem prover.

## Pages

- [ShotTx](readme.md)

## Modules

- [ShotTx.Proof.Step](ShotTx.Proof.Step.md): A single node in a `ShotTx.Proof` derivation tree.

- Public API
  - [ShotTx](ShotTx.md): Root module for `ShotTx`, the tableau component of the **Shot**
ecosystem — a Church Simple Type Theory (STT) automated theorem
prover. The `Tx` suffix stands for "Tableaux"; sibling packages
cover the shared data structures (`ShotDs`), higher-order unification
(`ShotUn`) and term ordering (`ShotTo`).
  - [ShotTx.Cli](ShotTx.Cli.md): Command-line entry point for the **Shot** prover, packaged as an escript.
  - [ShotTx.Config](ShotTx.Config.md): Session-global defaults for `ShotTx.Prover` calls.
  - [ShotTx.Data.Parameters](ShotTx.Data.Parameters.md): Proof-search configuration struct. All fields are keyword-settable via `struct!/2`.
  - [ShotTx.Proof](ShotTx.Proof.md): A tableau derivation reconstructed from the closed-branch traces returned
by the prover.
  - [ShotTx.Prover](ShotTx.Prover.md): Public entry point for the ShotTx tableau prover.

- Proof search core
  - [ShotTx.Prover.Branch](ShotTx.Prover.Branch.md): Pure functional core representing a single branch in the proof tree.
Applies rules and returns the resulting state and any intended side-effects
(Outbox pattern) for the stateful Worker to execute.
  - [ShotTx.Prover.Demodulation](ShotTx.Prover.Demodulation.md): Rewrite-to-normal-form under a set of NCPO-LNF-oriented equations,
restricted to rewrites that produce **no variable bindings**.
  - [ShotTx.Prover.FormulaPqueue](ShotTx.Prover.FormulaPqueue.md): Min-priority queue for tableau formulas, backed by `:gb_trees`.
  - [ShotTx.Prover.LambdaLift](ShotTx.Prover.LambdaLift.md): Lambda-lifting as a tableau α-rule.
  - [ShotTx.Prover.Paramodulation](ShotTx.Prover.Paramodulation.md): Utility helpers for term-DAG traversal used by
`ShotTx.Prover.Demodulation`.
  - [ShotTx.Prover.Rules](ShotTx.Prover.Rules.md): Tableau rule classification and priority costs.
  - [ShotTx.Prover.TermOrder](ShotTx.Prover.TermOrder.md): Two orderings on HOL term IDs, both parameterised by an `%ShotTo.Parameters{}`.
  - [ShotTx.Util.PropSimplify](ShotTx.Util.PropSimplify.md): Propositional simplification of HOL terms via binary decision diagrams.

- OTP / concurrency
  - [ShotTx.Prover.EtsKeeper](ShotTx.Prover.EtsKeeper.md): GenServer that owns the ETS tables for a single proof session.
  - [ShotTx.Prover.Manager](ShotTx.Prover.Manager.md): GenServer that orchestrates the proof search for a single session.
  - [ShotTx.Prover.SessionSupervisor](ShotTx.Prover.SessionSupervisor.md): OTP supervisor owning the per-session proof-search tree.
  - [ShotTx.Prover.Stats](ShotTx.Prover.Stats.md): Lightweight ETS-backed counters/samplers for proof-session debugging,
plus user-facing helpers to compile and pretty-print a snapshot.
  - [ShotTx.Prover.Worker](ShotTx.Prover.Worker.md): Long-lived worker process that steals branch data from an ETS queue,
processes it using the pure Branch module, and applies resulting side effects.

- Agents
  - [ShotTx.IsabelleBridge](ShotTx.IsabelleBridge.md): Application-level singleton that owns a warm Isabelle connection.
  - [ShotTx.Prover.ContradictionAgent](ShotTx.Prover.ContradictionAgent.md): GenServer that detects global closure and extracts countermodels.
  - [ShotTx.Prover.ModelAgent](ShotTx.Prover.ModelAgent.md): GenServer that plays the dual of `ContradictionAgent`: probes live branches
for satisfiability via an external model finder. A `:sat` verdict on any
branch terminates the session with a confirmed countermodel.
  - [ShotTx.Prover.ModelAgent.Backend](ShotTx.Prover.ModelAgent.Backend.md): Behaviour implemented by external model-finding backends.
  - [ShotTx.Prover.ModelAgent.Backend.Nitpick](ShotTx.Prover.ModelAgent.Backend.Nitpick.md): `Backend` that ships the branch's frontier to a warm Isabelle server and
runs `nitpick[satisfy]` against it.
  - [ShotTx.Prover.ModelAgent.Backend.Stub](ShotTx.Prover.ModelAgent.Backend.Stub.md): Trivial `Backend` implementation that returns `:unknown` for every probe.
Used when `model_agent_backend` is `:none`, `:stub`, or when Isabelle is
unavailable at runtime. Keeps the agent's plumbing exercised in tests
without any external dependency.

  - [ShotTx.Prover.ModelAgent.Frontier](ShotTx.Prover.ModelAgent.Frontier.md): Projects a `ShotTx.Prover.Branch` onto a `ShotDs.Data.Problem` for external
model-finding.
  - [ShotTx.Prover.Suggestion](ShotTx.Prover.Suggestion.md): A single instantiation hint produced by `SuggestionAgent` and consumed
by workers. Persisted in the `:suggestions` ETS table with the row shape
  - [ShotTx.Prover.SuggestionAgent](ShotTx.Prover.SuggestionAgent.md): A *peer* of `ContradictionAgent`. Subscribes to the same raw evidence
stream (`branch_evidence_<session>`) and runs strictly weaker unification
than CA — pair-level only — turning σs into per-recipe instantiation
hints.

- Generation
  - [ShotTx.Generation](ShotTx.Generation.md): Enumerates the closed HOL terms needed for γ-finite instantiation and
primitive substitution.
  - [ShotTx.Generation.GeneralBindings](ShotTx.Generation.GeneralBindings.md): Generates general bindings for primitive substitution.
  - [ShotTx.Generation.TypeUniverse](ShotTx.Generation.TypeUniverse.md): Collects and maintains the set of types relevant to a proof.
  - [ShotTx.Prover.Provenance](ShotTx.Prover.Provenance.md): Per-fresh-variable annotation recording which quantifier minted the
variable and on which branch. Consumed by `ContradictionAgent` and
`SuggestionAgent` to turn unifier evidence back into instantiation hints.

- Benchmarking
  - [ShotTx.Benchmark.Ablation](ShotTx.Benchmark.Ablation.md): Declarative ablation matrix for the ShotTx prover.
  - [ShotTx.Benchmark.TptpRunner](ShotTx.Benchmark.TptpRunner.md): Runs the prover across the TPTP TH0/TH1 problem library and records one CSV
row per problem. Designed for long unattended benchmark sweeps on a laptop

