Changelog

Copy Markdown View Source

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

[0.1.0] - 2026-08-18

Added

  • README section on the two operational properties that surprise callers: verdicts near the timeout are not reproducible, because a worker pool races on a shared queue under a wall-clock budget; and the node-wide :term_pool accumulates every term the node has seen until ShotTx.Prover.release_term_pool/0 clears it.

Changed

  • Dependencies bumped to shot_ds 1.3.1, shot_un 0.2.1 and shot_to 0.2.0.
  • Clearer gamma_finite labels; harder parse timeouts and a parse bug report.
  • Ablation-study driver improvements and the in-flight CSP counter.

Fixed

  • Demodulation rewrote connectives unsoundly.
  • Unsound models reported as CounterSatisfiable.
  • Unreliable termination and timeouts.
  • Resource leaks.
  • Parentless nodes in the proof-tree rendering.
  • The README and ShotTx.Config documented Prover.prove(problem, [], opts), which raises FunctionClauseError. A ShotDs.Data.Problem is proved through prove/2.
  • An unclosed code fence in the README swallowed the License section.

[0.0.3] - 2026-08-09

Supersedes the unreleased 0.0.2; entries cover everything since 0.0.1.

Added

  • ShotTx.Benchmark.HolSuite and HolRunner: 130 higher-order problems as canonical THF, one fresh BEAM per problem, CSV-scored.
  • scripts/run_hol_benchmark.sh and scripts/hol_problem.exs — resumable, with a STOP sentinel.
  • Global configuration options on ShotTx.Data.Parameters (worker pool size, ablation switches for the contradiction and suggestion agents).

Changed

  • Demodulation is restricted to ground equations. Rewriting with an equation carrying rigid γ-variables destroys the literal pair the CSP needs.
  • An exhausted rule queue is no longer reported as a countermodel. Branch.model_certain?/2 requires each same-head, opposite-polarity literal pair to be separated by two distinct rigid base-type terms; otherwise the branch is :exhausted and the session answers :unknown.
  • suggestions_enabled and prim_subst_after now default to true and 1.

Fixed

  • Unsound CounterSatisfiable on seven problems, from formulas queued before an equation arrived never being re-normalised under it.
  • Crash during proof reconstruction on :demodulation traces.
  • Two type errors that killed branches mid-search: prim-subst instantiation paired a head declaration with an instance typed by the applied term, and the suggestion agent published hints ill-typed against their recipe.
  • Iterative deepening stalled permanently once any branch saturated.
  • The manager's settle call was unbounded, so the timeout stopped applying.

[0.0.1] - 2026-08-04

Initial pre-release. API is unstable; expect breaking changes before 0.1.0.

Added

  • Parallel, actor-based tableau refutation search for higher-order logic (Church Simple Type Theory).
  • ShotTx.Prover public API: prove/1,2,3, sat/1,2,3, prove_string/1,2,3.
  • Iterative deepening over the γ-limit and primitive-substitution depth.
  • Global closure detection and SAT countermodel extraction via ShotTx.Prover.ContradictionAgent.
  • Ordered paramodulation with an NCPO-LNF term order (Niederhauser & Middeldorp, 2025).
  • TPTP TH0 / TH1 problem-file input; SZS-ontology output.
  • ShotTx.Cli escript entry point with --szs flag.
  • Proof reconstruction with text and Mermaid renderers.
  • ShotTx.Benchmark.TptpRunner for resumable, CSV-scored TPTP sweeps.