Modules
Declarative ablation matrix for the ShotTx prover.
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
Command-line entry point for the Shot prover, packaged as an escript.
Session-global defaults for ShotTx.Prover calls.
Proof-search configuration struct. All fields are keyword-settable via struct!/2.
Enumerates the closed HOL terms needed for γ-finite instantiation and primitive substitution.
Generates general bindings for primitive substitution.
Collects and maintains the set of types relevant to a proof.
Application-level singleton that owns a warm Isabelle connection.
A tableau derivation reconstructed from the closed-branch traces returned by the prover.
A single node in a ShotTx.Proof derivation tree.
Public entry point for the ShotTx tableau prover.
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.
GenServer that detects global closure and extracts countermodels.
Rewrite-to-normal-form under a set of NCPO-LNF-oriented equations, restricted to rewrites that produce no variable bindings.
GenServer that owns the ETS tables for a single proof session.
Min-priority queue for tableau formulas, backed by :gb_trees.
Lambda-lifting as a tableau α-rule.
GenServer that orchestrates the proof search for a single session.
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.
Behaviour implemented by external model-finding backends.
Backend that ships the branch's frontier to a warm Isabelle server and
runs nitpick[satisfy] against it.
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.
Projects a ShotTx.Prover.Branch onto a ShotDs.Data.Problem for external
model-finding.
Utility helpers for term-DAG traversal used by
ShotTx.Prover.Demodulation.
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.
Tableau rule classification and priority costs.
OTP supervisor owning the per-session proof-search tree.
Lightweight ETS-backed counters/samplers for proof-session debugging, plus user-facing helpers to compile and pretty-print a snapshot.
A single instantiation hint produced by SuggestionAgent and consumed
by workers. Persisted in the :suggestions ETS table with the row shape
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.
Two orderings on HOL term IDs, both parameterised by an %ShotTo.Parameters{}.
Long-lived worker process that steals branch data from an ETS queue, processes it using the pure Branch module, and applies resulting side effects.
Propositional simplification of HOL terms via binary decision diagrams.