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

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

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, :traces, :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), paramodulation.
• 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.

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

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.

License

See LICENSE.