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.
• 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

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    # + reconstructed proof tree
./shot_tx --szs -t 30000 problem.p   # 30-second wall-clock budget

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 PUZ001+1.p
% SZS status CounterSatisfiable for SET001+3.p
% SZS status Timeout for HOL024^4.p
% SZS status GaveUp for LCL083-1.p

Exit codes: 0 for Theorem / CounterSatisfiable, 1 for GaveUp / Timeout, 2 for parsing or option errors — matching the convention used by the CASC prover competitions.

Command-line reference

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

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("PUZ001+1.p", :tptp_problem)
Prover.prove(problem, timeout: 30_000)

# Ask for satisfiability instead.
Prover.sat(problem_formulas, 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 and CounterSatisfiable 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.

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:

The full table (with all 33 fields) 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_ROOT=/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.