ShotTx.Prover (ShotTx v0.0.1)

Public entry point for the ShotTx tableau prover.

Three related APIs live here:

prove/1, prove/2, prove/3 — attempt to prove conclusion from assumptions (or a ShotDs.Data.Problem). Returns a proof_result/0.
sat/1, sat/2, sat/3 — check a list of formulas for satisfiability without negating a conclusion. Returns the raw Manager result.
prove_string/1, prove_string/2, prove_string/3 — thin convenience wrapper that formats the outcome via format_result/1.

Every call spins up a fresh ShotTx.Prover.SessionSupervisor and blocks synchronously on the Manager until the search terminates (theorem, countermodel, timeout, or exhausted iterative deepening). Configuration is threaded through as a keyword list that is merged into a ShotTx.Data.Parameters struct — see that module for the full list of knobs, and ShotTx.Config for session-wide defaults.

Summary

Types

proof_result()

Functions

compile_stats(stats)

Compiles a raw stats snapshot (as returned by prove/3 with stats: true) into a structured report grouped by :timing, :search, :rules, :branches, and :csp. Idempotent on already-compiled reports.

format_result(arg1)

Formats a proof_result() as a short human-readable string for quick inspection.

format_stats(stats, opts \\ [])

Pretty-prints a stats snapshot or compiled report. Pass verbose: true to include zero-valued rule/branch counters, or sections: [:timing, :csp] to render a subset.

prove(problem)

Shorthand delegating to the three-argument form.

prove(conclusion, opts)

prove(conclusion, assumptions, opts)

Attempts to prove conclusion from assumptions.

prove_string(target, assumptions \\ [], opts \\ [])

Convenience wrapper that returns a human-readable string result, preserving the original prove interface for quick testing.

sat(formulas, defs \\ %{}, opts \\ [])

Checks the satisfiability of a list of formulas. Delegates the execution to the Manager GenServer.

Types

proof_result()

@type proof_result() ::
  {:thm, ShotTx.Proof.t()}
  | {:csa, String.t(), ShotTx.Proof.t()}
  | :unknown
  | {:timeout, ShotTx.Proof.t()}
  | {:error, term()}

Functions

compile_stats(stats)

@spec compile_stats(map()) :: map()

Compiles a raw stats snapshot (as returned by prove/3 with stats: true) into a structured report grouped by :timing, :search, :rules, :branches, and :csp. Idempotent on already-compiled reports.

format_result(arg1)

@spec format_result(proof_result()) :: String.t()

Formats a proof_result() as a short human-readable string for quick inspection.

format_stats(stats, opts \\ [])

@spec format_stats(
  map(),
  keyword()
) :: String.t()

Pretty-prints a stats snapshot or compiled report. Pass verbose: true to include zero-valued rule/branch counters, or sections: [:timing, :csp] to render a subset.

prove(problem)

@spec prove(ShotDs.Data.Problem.t() | ShotDs.Data.Term.term_id()) :: proof_result()

Shorthand delegating to the three-argument form.

Accepts either a ShotDs.Data.Problem (prove(problem) — no options), a single ShotDs.Data.Term.term_id/0 conclusion (prove(conclusion)), or a conclusion plus either an assumption list or options list.

See prove/3 for the primary interface and return type.

prove(conclusion, opts)

@spec prove(
  ShotDs.Data.Problem.t(),
  keyword()
) :: proof_result() | {proof_result(), map()}

@spec prove(ShotDs.Data.Term.term_id(), [ShotDs.Data.Term.term_id()] | keyword()) ::
  proof_result() | {proof_result(), map()}

prove(conclusion, assumptions, opts)

@spec prove(ShotDs.Data.Term.term_id(), [ShotDs.Data.Term.term_id()], keyword()) ::
  proof_result() | {proof_result(), map()}

Attempts to prove conclusion from assumptions.

Accepts three call shapes:

prove(problem) — a Problem struct with a conjecture and axioms.
prove(conclusion) / prove(conclusion, assumptions) — term IDs.
prove(conclusion, assumptions, opts) — full form; opts are forwarded to Parameters except for the :defs key (a definition map).

Returns a proof_result().

prove_string(target, assumptions \\ [], opts \\ [])

@spec prove_string(
  ShotDs.Data.Problem.t() | ShotDs.Data.Term.term_id(),
  [ShotDs.Data.Term.term_id()],
  keyword()
) :: String.t()

Convenience wrapper that returns a human-readable string result, preserving the original prove interface for quick testing.

sat(formulas, defs \\ %{}, opts \\ [])

@spec sat([ShotDs.Data.Term.term_id()] | ShotDs.Data.Term.term_id(), map(), keyword()) ::
  {:sat, map()}
  | {:unsat, map(), list(), map()}
  | {:unknown, term()}
  | {:timeout, ShotTx.Proof.t()}
  | {sat_result :: term(), stats :: map()}

Checks the satisfiability of a list of formulas. Delegates the execution to the Manager GenServer.