ShotTx

Shot is a Church Simple Type Theory (STT) automated theorem prover. This package, ShotTx, is the tableau component of the Shot ecosystem — the Tx suffix reads as "Tableaux". Sibling packages cover the data structures (ShotDs), higher-order unification (ShotUn) and term ordering (ShotTo) that the prover builds on.

Shot performs automated theorem proving for higher-order logic (HOL) via a parallel, actor-based refutation search with iterative deepening, Skolemisation, primitive substitution, and demodulation.

Written for a Master's thesis on parallel HOL tableau reasoning (jcschuster/shot-thesis). The thesis describes v0.1.1, archived as 10.5281/zenodo.23044601.
Reads TPTP TH0 / TH1 problem files or plain THF formulas.
Emits either a short human-readable verdict or SZS-ontology status lines compatible with the standard prover output format used by Vampire, E, Leo-III, etc.
Runnable both as a library and as a stand-alone escript.

Quick start

Build

mix deps.get
mix compile
mix escript.build          # produces the `shot_tx` executable (needs Erlang/OTP)

A self-contained package (bundled Erlang runtime, started via bin/shot) is built with the Containerfile:

podman build --target dist -o dist .   # dist/Shot---<version>.tgz (SystemOnTPTP)
                                       # dist/Shot---<version>-starexec.tgz (StarExec)

Solve a problem

./shot_tx problem.p                  # short output: THM / CSA / UNK / Timeout / ...
./shot_tx --szs problem.p            # SZS status line
./shot_tx --szs --proof problem.p    # + proof tree in an SZS output block
./shot_tx --szs -t 30000 problem.p   # 30-second wall-clock budget for the whole run
./shot_tx --szs --cpu-timeout 30000 problem.p   # 30 CPU-seconds instead (all cores summed)

include directives and relative problem paths are resolved against $TPTP (or $TPTP_ROOT):

TPTP=/opt/TPTP ./shot_tx --szs Problems/SYO/SYO002^1.p

Inline problems and stdin are also accepted:

./shot_tx "thf(em, conjecture, ! [P: \$o] : (P | ~P))."
echo "P | ~P" | ./shot_tx -

Sample SZS output

% SZS status Theorem for SYO002^1.p
% SZS status WCTimeout for SYO001^1.p
% SZS status Inappropriate for PUZ001+1.p : Unexpected token: 'fof' (:atom)

With --proof, the proof follows in a Proof block. For a countermodel the block is a Model: the model comes first, then the open branch:

% SZS status CounterSatisfiable for pq.p
% SZS output start Model for pq.p
p, ¬q
1. ¬(p ⊃ q)                         [given]
2. p ∧ (¬q)                         [bdd⊢ on 1]
3. p                                [∧ on 2]
4. ¬q                               [∧ on 2]
5. ★ open                           [model: p, ¬q]
% SZS output end Model for pq.p

The block is Shot's own derivation tree, not a TSTP derivation. Outside the output blocks every stdout line is a % comment.

Status	When	Exit
`Theorem` / `CounterSatisfiable`	Problem has a conjecture	0
`Unsatisfiable` / `Satisfiable`	No conjecture, or `--sat`	0
`Incomplete`	Search space exhausted without a model	1
`GaveUp`	A model could not be trusted (below), internal error, other	1
`WCTimeout`	Wall-clock limit (`-t`) reached	1
`Timeout`	CPU-time limit (`--cpu-timeout`) reached	1
`Forced`	Stopped by SIGTERM	1
`Inappropriate`	Input is not THF Shot can parse (e.g. FOF/CNF)	2
`InputError`	Missing file, unreadable include	2
`UsageError`	Bad command-line options (also explained on stderr)	2

An internal error is reported as GaveUp with the reason after :. Problems using $ite are rejected as Inappropriate (Shot would treat it as an uninterpreted constant, which is sound for proofs but not for models).

SystemOnTPTP and StarExec

Shot is listed as Prover, for TH0_NAR. SystemOnTPTP limits are CPU seconds, so its command line is

bin/shot --szs --proof --cpu-timeout <seconds>000 <problem>

with $TPTP set for includes. StarExec runs bin/starexec_run_default, which takes the problem as $1 and the wall-clock limit from $STAREXEC_WALLCLOCK_LIMIT; the Shot---<version>-starexec.tgz archive has bin/ at its root, as StarExec requires. Both packages bundle the Erlang runtime (built for Ubuntu 24.04 / glibc 2.39) and libsctp, and run on a host without Erlang. bin/shot disables crash dumps and core files, so a run killed by a signal leaves nothing behind.

System description:

Shot is a parallel free-variable tableau prover for TH0 (Church's simple type theory), written in Elixir. Countermodels are reported only for problems whose types are all Boolean. Proofs are Shot's own derivation trees in an SZS Proof block, not TSTP derivations.

Command-line reference

shot_tx [OPTIONS] <FILE | "STRING" | ->

Flag	Description
`--szs`	Emit `% SZS status <verdict> for <name>`
`--sat`	Check satisfiability instead of proving (skip conjecture negation)
`--proof`	Print the reconstructed proof / countermodel
`--stats`	Print search statistics after the result
`-t`, `--timeout MS`	Wall-clock budget for the whole run (default 5000)
`-v`, `--verbose`	Enable prover debug logging on stderr
`-h`, `--help`	Show the full option listing

All fields of ShotTx.Data.Parameters are exposed as long flags in kebab-case; boolean parameters accept --flag / --no-flag. For the authoritative list run ./shot_tx --help or see the ShotTx.Data.Parameters module docs.

Library usage

import ShotDs.Hol.Sigils
alias ShotDs.Tptp
alias ShotTx.Prover

# Prove a THF formula directly (no axioms).
Prover.prove(~f"![P : $o]: (P | ~P)")
#=> {:thm, %ShotTx.Proof{...}}

# Parse and prove a TPTP problem.
{:ok, problem} = Tptp.parse_tptp_file("SYO/SYO002^1.p", :tptp_problem)
Prover.prove(problem, timeout: 30_000)

# Refute a formula set as given (no conjecture is negated).
# {:thm, proof} means unsatisfiable, {:csa, model, proof} satisfiable.
Prover.refute(formulas, defs: definitions, timeout: 10_000)

Session-wide defaults can be set with ShotTx.Config:

ShotTx.Config.configure(timeout: 30_000, suggestions_enabled: true)
Prover.prove(problem)                    # uses the globals
Prover.prove(problem, timeout: 1_000)    # per-call still wins

See ShotTx.Prover for the full public API and ShotTx.Proof for proof-tree inspection (text / Mermaid renderers).

Operational notes

Two properties of the prover surprise people who treat it as a pure function from problem to verdict. Neither is a bug, but both change how you should call it.

Verdicts are not reproducible near the timeout

Proof search is parallel: a pool of workers races on a shared queue, and the answer depends on which worker closes a branch first inside the wall-clock budget. A problem that needs almost all of its budget may be decided on one run and time out on the next, on the same input and the same settings.

A 10,062-run probe over the TPTP corpus repeated 3,354 problem / configuration pairs. 84 of them (2.5%) answered differently across repeats, and every one of those was Theorem versus Timeout — the budget ran out, not the calculus changing its mind. No problem was ever decided two different ways.

So Timeout and GaveUp mean "not decided within this budget", not "not provable"; only Theorem, CounterSatisfiable, Unsatisfiable and Satisfiable are claims about the problem. If you need repeatable runs, give the search enough headroom that it is not finishing at the edge of the budget, and set worker_pool_size: 1 to remove the scheduling race — the wall clock still bounds the search, so a problem right at the limit can still flip.

The term pool grows across proofs

ShotDs hash-conses every term into :term_pool, a node-wide ETS table. A session frees its own tables when it exits, but the term pool is shared and only ever grows: it accumulates every term of every problem the node has seen. Measured on repeated proofs of one problem, ETS grew by roughly 0.7 MB per proof and was never reclaimed — 2 MB to 23 MB over 30 proofs.

This never matters for the escript, which is one fresh BEAM per problem. It matters for a long-lived node — a Livebook session, a benchmark sweep, an application that keeps proving. Reclaim it with:

ShotTx.Prover.release_term_pool()

Term IDs do not survive a release: any ShotTx.Proof, ShotDs.Data.Problem or bare term ID you are still holding becomes unreadable. Call it between problems, once you have consumed the previous result.

Architecture

The prover implements a distributed tableau calculus. Proof search is split across concurrent worker processes that operate on immutable branch snapshots, with shared state held in per-session ETS tables.

ShotTx.Prover (public API)
  └─ SessionSupervisor (per-proof OTP tree)
       ├─ EtsKeeper           — owns :stats, :tombs, :work_queue, :idle_queue,
       │                        :idle_workers, :traces, :provenance, :suggestions
       ├─ Manager             — spawns N workers, drives iterative
       │                        deepening, owns the result
       ├─ ContradictionAgent  — global closure via unification CSP
       ├─ SuggestionAgent     — instantiation hints from local clashes
       ├─ ModelAgent          — optional Nitpick-backed model finder
       └─ DynamicSupervisor → Worker × N
                                └─ Branch.step/4  (pure functional core)

Tableau rules: α (linear), β (branching), γ / γ-finite (universal instantiation with reinsertion), δ (Skolemisation), primitive substitution (iterative deepening on general bindings), atomic clash detection, equality expansion (o-type iff / extensional / Leibniz), demodulation (binding-free equational rewriting).
Iterative deepening: γ-limit and prim-subst depth start at 1 and grow whenever all workers stall.
Global closure: ContradictionAgent unifies clashes across every open branch through the shot_un CSP.
SAT exit: a branch with an empty queue and no sleeping γ-rules is saturated; the agent extracts a countermodel.

Countermodels are conservative

A saturated branch is only a model if bounded γ-instantiation cannot have missed an instance. That is guaranteed when every type in the problem is pure-o ($o, $o>$o, …), whose domains are finite and enumerated. For any other problem a saturated branch is reported as :unknown (GaveUp). Pass pure_o_models_only: false (--no-pure-o-models-only) to get the v0.1 behaviour, which reports every saturated branch.

See the ShotTx.Prover.* module documentation for the details of every component. Rendered docs are produced by mix docs.

Configuration

All proof-search knobs live in the ShotTx.Data.Parameters struct. The common ones:

Field	Default	Purpose
`timeout`	`5_000`	Wall-clock ms before returning `:timeout`
`initial_gamma_limit`	`1`	Starting γ-rule instantiation depth
`initial_prim_limit`	`1`	Starting primitive-substitution binding depth
`unfold_defs`	`:lazy`	`:eager` unfolds definitions immediately
`demodulation`	`true`	Binding-free equational rewriting (forward + backward)
`equivalence_processing`	`:bidirectional_imp`	`↔` expansion mode: `:same_polarity`, `:bidirectional_imp`, or `:dual`
`contradiction_agent`	`true`	Enable global CSP-based closure
`worker_pool_size`	`:auto`	`System.schedulers_online()`
`iterative_deepening`	`true`	Whether to bump limits when workers stall
`formula_cost_strategy`	`:default`	`:default`, `:uniform`, `:depth_first`, `{:custom, fn}`
`pure_o_models_only`	`true`	Only report countermodels for pure-`o` problems (see above)

The full table is in ShotTx.Data.Parameters's moduledoc. The soundness argument for why ShotTx does binding-free demodulation instead of classical paramodulation lives in ShotTx.Prover.Paramodulation's moduledoc — the rigid-variable tableau architecture requires that free-variable commitments be reconciled globally by ContradictionAgent, not locally by a rewrite rule.

Testing and quality

mix test
mix credo --all
mix dialyzer
mix format

Interactive examples live in examples/ as Livebook notebooks; they are the primary test harness while the formal test suite grows.

An ablation-study driver over the TPTP TH0 / TH1 corpus is included:

export TPTP=/path/to/TPTP
./scripts/run_ablation.sh

The full sweep is a multi-day run, so validate the corpus first with a short pass — a TPTP-version mismatch surfaces as parser_error rows:

PROBLEM_LIMIT=20 ./scripts/run_ablation.sh smoke_results
grep -c parser_error smoke_results/baseline.csv

Parsing and proving each run under a hard wall-clock budget (PARSE_TIMEOUT, default 60s; BASE_TIMEOUT + PROVE_GRACE for the proof attempt), so no single problem can stall the sweep — a few TPTP problems pull in enough includes to keep the parser busy for many minutes. A killed phase still yields a CSV row (parse_timeout / hard_timeout), and unparsable problems are recorded in <output_dir>/parse_cache so later configurations replay the verdict instead of re-parsing.

See ShotTx.Benchmark.Ablation and ShotTx.Benchmark.TptpRunner for the sweep matrix and per-problem CSV format.

Dependencies

shot_ds — HOL data structures, term factory, TPTP / THF parser, semantics.
shot_un — higher-order unification and CSP solver.
shot_to — NCPO term ordering.
isabelle_elixir (optional) — enables the ShotTx.Prover.ModelAgent.Backend.Nitpick backend.

Installation

This package can be installed by adding shot_tx to your list of dependencies in mix.exs:

def deps do
  [
    {:shot_tx, "~> 0.1"}
  ]
end

License

See LICENSE.