shot_tx

# ShotTx

[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.23044599.svg)](https://doi.org/10.5281/zenodo.23044599)

**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](https://github.com/jcschuster/shot-thesis)). The
  thesis describes v0.1.1, archived as
  [10.5281/zenodo.23044601](https://doi.org/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

```bash
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`:

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

### Solve a problem

```bash
./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`):

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

Inline problems and stdin are also accepted:

```bash
./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

```elixir
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`:

```elixir
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:

```elixir
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

```bash
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:

```bash
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:

```bash
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 `include`s 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`](https://hex.pm/packages/shot_ds) — HOL data
  structures, term factory, TPTP / THF parser, semantics.
- [`shot_un`](https://hex.pm/packages/shot_un) — higher-order
  unification and CSP solver.
- [`shot_to`](https://hex.pm/packages/shot_to) — NCPO term ordering.
- [`isabelle_elixir`](https://hex.pm/packages/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`:

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

---

## License

See `LICENSE`.