Thesis Defense

Mix.install([
  {:shot_tx, "0.1.0"},
  {:kino, "~> 0.19.1"}
])

⠀

This Livebook is meant to be displayed in presentation mode (enable it under View → Presentation in the lower right-hand corner). Some useful shortcuts: j and k are for next/previous cell and double-tapping e executes the current code cell.

UNIVERSITY OF BAMBERG Applied Computer Science Degree Program in the
Faculty of Information Systems and Applied Computer Sciences Master's Thesis Defense Extensionality and Instance-based Methods in
Tableau-based Higher-Order Automated Theorem Proving by Johannes Schuster Supervisor
Prof. Dr. Christoph Benzmüller Chair for AI Systems Engineering 18 August 2026

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Contributions

---

• A binding-free formulation of a free-variable tableau calculus for simply-typed higher-order logic
• A concurrent actor architecture on the BEAM as implementation prototype
• Implementation of infrastructure, including data structures, parsing, unification and term ordering
• Four publicly available Hex packages: shot_ds, shot_un, shot_to, and shot_tx
• Interactive material (Livebooks) for demonstration and education purposes, including the Livebook version of the thesis
• An ablation study over different components of the prover
• A qualitative evaluation over a structured set of higher-order problems (Benzmüller & Brown, 2005)

Sʜᴏᴛ and its Foundation

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

The Logic in Question

---

(Monomorphised) Simple Types

$$ \mathcal{B} = {\iota, o} \uplus \mathcal{A} \qquad\qquad\qquad \bar\tau_n{\to}\varsigma \in \mathcal{T}\quad\text{ if $\bar\tau_n \in \mathcal{T}$ with $n \geq 0$ and $\varsigma \in \mathcal{B}$} $$

$\mathcal{A}$: type variables, treated as rigid base types

---

Terms

$$ s, t \coloneqq c\langle\bar\rho\rangle \mid X \mid p \mid i \mid \lambda \bar\tau., t \mid s(\bar t) $$

$c$: constant symbol from signature, $\bar\rho, \bar\tau \in \mathcal{T}$, $X$: variable symbol, $p$: parameter, $i \in \N_{> 0}$: de Bruijn index

---

Signature

$$ \top, \bot : o \qquad\qquad \neg : o !\to! o \qquad\qquad \lor, \land, \supset, \equiv ;: (o, o) {\to} o $$

$$ \forall,\exists : [\alpha]., (\alpha {\to} o) {\to} o \qquad\qquad =; : [\alpha]., (\alpha, \alpha) {\to} o $$

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Term Representation and Parsing

---

Data Structures

• Terms in $\beta\eta$-long normal form, normalised after every transformation
• Spine representation (uncurried)
• Bookkeeping fields for caching
  • :fvars, :consts, :tvars, :max_num
• Hash consing: terms are only created once with distinct ID

Parsing THF

• Recursive descent with algorithm W-style type inference (supports Hindley-Milner-like polymorphism)
• Sigils allow for quick parsing of THF as a DSL

import ShotDs.Hol.Sigils
~g{ ^[X: $o]: ( P & X ) }

alias ShotDs.Stt.TermFactory, as: TF
term = TF.get_term! ~g{ ^[X: $o]: ( P & X ) }
Kino.Tree.new term

Kino.Layout.grid for a <- term.args, do: Kino.Tree.new TF.get_term! a

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

The Calculus: Standard Expansion Rules

---

Sʜᴏᴛ constructs standard free-variable refutation tableaux:

For proof goal $\Phi \models \psi$, show that $\Phi \cup {\neg \psi}$ is unsatisfiable (has a closed tableau).

---

$\alpha$- and $\beta$-rules:

$$ \frac{\neg\neg \varphi}{\varphi}(\neg\neg) \qquad\qquad \frac{\varphi \land \psi}{\begin{gathered}\varphi \ \psi\end{gathered}}(\land) \qquad\qquad \frac{\neg (\varphi \lor \psi)}{\begin{gathered}\neg \varphi \ \neg \psi\end{gathered}}(\neg\lor) \qquad\qquad \frac{\neg(\varphi \supset \psi)}{\begin{gathered}\varphi \ \neg \psi\end{gathered}}(\neg!\supset) $$

$$ \frac{\varphi \lor \psi}{\varphi \mid \psi}(\lor) \qquad \frac{\neg(\varphi \land \psi)}{\neg\varphi \mid \neg\psi}(\neg\land) \qquad \frac{\varphi \supset \psi}{\neg\varphi \mid \psi}(\supset)\qquad \frac{\varphi \equiv \psi}{\begin{gathered}\varphi \supset \psi \ \psi \supset \varphi\end{gathered}}(\equiv) \qquad \frac{\neg(\varphi \equiv \psi)}{\neg(\varphi \supset \psi) \mid \neg(\psi \supset \varphi)}(\neg!\equiv) $$

$\beta$-variation, as $\varphi \lor \psi \equiv \varphi \lor (\psi \land \neg \varphi)$:

$$ \frac{\beta}{\begin{array}{c|c}\beta_1 & \beta_2 \ & \neg\beta_1\end{array}}(\beta\text{-var}) $$

$\gamma$-rules ($X$ is a fresh variable symbol):

$$ \frac{\forall \tau., \Phi}{\begin{array}{c}\Phi(X!:!\tau) \ \forall \tau., \Phi\end{array}}(\forall) \qquad\qquad \frac{\neg(\exists \tau., \Phi)}{\begin{array}{c}\neg (\Phi(X!:!\tau)) \ \neg(\exists \tau., \Phi)\end{array}}(\neg\exists) $$

$\delta$-rules ($\mathbf{s}$ is a fresh Skolem term for $\Phi$):

$$ \frac{\exists \tau., \Phi}{\Phi(\mathbf{s})}(\exists) \qquad\qquad \frac{\neg(\forall \tau., \Phi)}{\neg(\Phi(\mathbf{s}))}(\neg\forall) $$

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Binding-Freeness as Paradigm and Demodulation

---

• All rules are implemented to be binding-free, i.e., no variable is ever bound.
• Branch closure requiring non-empty substitution only happens simultaneously and unifiers are only computed jointly.
• Disagreement on literals is recorded as candidate.
• Search space for simultaneous unification: Cartesian product over all candidates of all branches.

This discipline allows a restricted version of demodulation to be adapted from superposition calculi. Under the equational theory $\mathcal{E}(\mathfrak{B})$ of a branch $\mathfrak{B}$ and reduction order $\succ$:

$$ \frac{\begin{gathered}\mathcal{E}(\mathfrak{B}) \ u\end{gathered}}{u{\downarrow}_{\mathcal{E}(\mathfrak{B})}^\succ}(\mathrm{demod}) $$

To keep demodulation binding free, we only consider ground oriented equations in $\mathcal{E}(\mathfrak{B})$.

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Equality Decomposition (Kohlhase, 1995)

---

So far, the rules can't handle a single equation without context. In these cases, we need to decompose in terms of Leibniz equality and extensionality ($\varsigma \in \mathcal{B} \setminus {o}$):

$$ \frac{\varphi =!\langle o\rangle; \psi}{\varphi \equiv \psi}(=!\langle o\rangle) \qquad \frac{s =!\langle \varsigma\rangle; t}{\forall \varsigma {\to} o.,1(s) \equiv 1(t)}(=!\langle \varsigma\rangle) \qquad \frac{s =!\langle (\tau, \bar{\upsilon}) {\to} \varsigma\rangle; t}{\forall \tau., s(1) =!\langle\bar{\upsilon} {\to} \varsigma\rangle; t(1)}(=!\langle(\tau, \bar{\upsilon}) {\to} \varsigma\rangle) $$

$$ \frac{\neg(\varphi =!\langle o\rangle; \psi)}{\neg(\varphi \equiv \psi)}(\neg!=!\langle o\rangle) \qquad \frac{\neg(s =!\langle \varsigma\rangle; t)}{\neg(\forall \varsigma {\to} o.,1(s) \equiv 1(t))}(\neg!=!\langle \varsigma\rangle) \qquad \frac{\neg(s =!\langle (\tau, \bar{\upsilon}) {\to} \varsigma\rangle; t)}{\neg(\forall \tau., s(1) =!\langle\bar{\upsilon} {\to} \varsigma\rangle; t(1))}(\neg!=!\langle(\tau, \bar{\upsilon}) {\to} \varsigma\rangle) $$

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Boolean Extensionality via Subformula Renaming and Instantiation

---

When a literal $\varphi$ has a rigid subformula $t$ of finite domain at position $\pi$, nothing will guess its value. The following two rules allow for canonical expansion in these cases and combined give boolean extensionality:

$$ \frac{\varphi}{\begin{gathered}\varphi[\mathbf{s}]\pi \ \mathbf{s} =!\langle\tau\rangle; t\end{gathered}}(\mathrm{rename}) \qquad\qquad \frac{\varphi}{\varphi[b_1]\pi \mid \dots \mid \varphi[b_k]_\pi}(\mathrm{inst}) $$

The rule $(\mathrm{inst})$ fires when $\varphi|_\pi$ is headed by parameter (or user-defined constant) $c : \tau$ and $\mathcal{D}(\tau) = {b_1, \dots, b_k}$. $\tau$ needs to be a pure $o$-type. A proof of $p(a) \land p(b) \supset p(a \land b)$ shows this at work:

import ShotTx.Prover
Logger.configure level: :error

opts = [beta_variant: false, unfold_defs: :eager]

with {:thm, proof} <- prove(~f{ (p @ a & p @ b) => p @ (a & b) }, opts) do
  Kino.Mermaid.new ShotTx.Proof.to_mermaid proof
end

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

γ-Instantiation: Finite Domains and Primitive Substitution

---

Finite domains can be enumerated without introducing variables and therefore inter-branch dependencies.

For pure $o$-type $\tau$ with $\mathcal{D}(\tau) = {b_1, \dots, b_n}$:

$$ \frac{\forall \tau., \Phi}{\begin{gathered}\Phi(b_1) \ \vdots \ \Phi(b_k)\end{gathered}}(\forall_{\mathrm{fin}}) \qquad\qquad \frac{\neg(\exists \tau., \Phi)}{\begin{gathered}\neg\Phi(b_1) \ \vdots \ \neg\Phi(b_k)\end{gathered}}(\neg\exists_{\mathrm{fin}}) $$

When $\tau$ is an impure $o$-type, i.e., with goal $o$, its (infinite) domain can be enumerated by general bindings.

$$ \frac{\forall \tau., \Phi}{\Phi(G_1) \mid \dots \mid \Phi(G_j)}(\mathrm{prim}) $$

For type $\iota{\to}o$, this might be the term $\lambda\iota., H_1(1) \land H_2(1)$ or just $\lambda\iota.,\bot$.

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Agents

---

ContradictionAgent:

• collects branch-local disagreement pairs and solves for common unifier
• most important closure mechanism
• independent process listening to a PubSub topic

SuggestionAgent:

• listens to the same topic
• computes unifiers and suggests solutions as $\gamma$-instantiations

ModelAgent:

• checks a branch for satisfiability, externally via nitpick
• a satisfiable branch yields a countermodel (⇒ another path to CSA)
• off by default, not evaluated

Kino.Mermaid.new """
graph TD
  SS["SessionSupervisor<br/>(:rest_for_one)"]
  EK["EtsKeeper<br/>owns session tables"]
  TS["Task.Supervisor<br/>async CSP dispatches"]
  MG["Manager<br/>orchestration + deepening"]
  CA["ContradictionAgent<br/>global closure (CSP)"]
  SA["SuggestionAgent<br/>heuristic hints (opt-out)"]
  MA["ModelAgent<br/>satisfiability probes (opt-in)"]
  BS["DynamicSupervisor<br/>worker pool"]
  W1["Worker 1"]
  W2["Worker 2"]
  WN["Worker N"]

  SS --> EK
  SS --> TS
  SS --> MG
  SS --> CA
  SS --> SA
  SS --> MA
  SS --> BS
  BS --> W1
  BS --> W2
  BS --> WN

  classDef keeper fill:#e3f2fd,stroke:#1565c0,color:#0d47a1;
  classDef agent fill:#e8f5e9,stroke:#2e7d32,color:#1b5e20;
  classDef worker fill:#eeeeee,stroke:#999999,color:#333333;
  class EK keeper;
  class CA,SA,MA agent;
  class W1,W2,WN worker;
"""

Evaluation: Ablation and Qualitative Investigation

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Ablation Study over TPTP-v9.3.0

---

• 5109 problems in TH0 and TH1 syntax
• 4183 reached the prover (after removing 628 parse timeouts, 221 parse errors and 77 without conjecture)
• timeout 2000 ms, default parameters as baseline (untuned)
• 16 configurations
• Baseline solved 685 (THM) + 62 (CSA)
• Union over 16 configs: 905 vs. 747 ⇒ baseline untuned
• Components contributing most:
  • ContradictionAgent: $-364$
  • Iterative deepening: $-87$
  • Demodulation: $-41$
  • Eager definition unfolding: $+48$

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Gretchen Question: Worker Pool vs. Single Worker

---

• Comparison over 3383 problems, both configurations exhausted budget

• Worker pool size 8 vs. 1

• Pool: $3.27\times$ inference steps, $3.13\times$ local branch closure

• However, only $1.17\times$ global searches with only $0.46$ closure searches per $1000$ steps vs. $1.28$ (serial)

• Pool is only $1.28\times$ faster on 705 solved problems

  ⇒ ContradictionAgent is already overwhelmed with one worker, a closure search takes nearly half the time budget

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Evaluation over Benzmüller & Brown (2005)

---

• Structured evaluation wrt. model classes
• 130 problems, including notions of equality, Boolean and functional extensionality, set theory, Cantor's theorem
• $76$-$79$ were proved (non-determinism from message passing)
• Sʜᴏᴛ was not able to prove problems from model classes $\mathfrak{M}{\beta\xi}$ and $\mathfrak{M}{\beta\mathfrak{f}}$ (functional extensionality)

Discussion and Future Work

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Limitations: Architecture, Implementation and Theoretical Limitations

---

• ContradictionAgent is currently too weak

  ⇒ Make unification more performant (concurrency, more decidable fragments etc.), or keep partial solutions (à la Giese, 2001)

  ⇒ Parallel searches over disjoint branch subsets

  ⇒ Better problem formulation, not naive cartesian product over candidates

• Recursive descent parser is too slow for larger files

  ⇒ work in progress: lazy LALR(1) parser, generated from TPTP's SyntaxBNF

• Calculus lacks functional extensionality ⇒ unification constraint or expansion rule:

$$ \frac{\begin{gathered}P(\bar{s}_n) \ \vdots \ \neg P(\bar{t}_n)\end{gathered}}{\neg(s_1 =!\langle\tau_1\rangle; t_1) ;\mid; \cdots ;\mid; \neg(s_n =!\langle\tau_n\rangle; t_n)}(\mathrm{ext}) $$

• A completeness argument is not established

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Future Work and Work in Progress

---

• Investigation into data structures ⇒ $\eta$-long or $\eta$-short form?
• Concurrency without binding-freeness
• Extending the signature with choice
• Experiments with complete signature over $o{\to}o$ and $(o, o){\to}o$
• Proper evaluation of ModelAgent
• Adapt SZS and TPTP proof objects

Work in Progress

• Efficient and properly TPTP-ground parser (tptp package)
• Memory-efficient, but stateless data structures

Take-Home

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Take-Home Messages

---

Binding-free tableaux move closure out of the branch

• No rule commits to a value for a free variable; branches only publish closure evidence
• Global closure is one constraint problem, solved by the ContradictionAgent
• Measured: it accounts for about half of all refutations ($-364$ of $682$)

Extensionality is bounded

• Boolean extensionality via renaming and instantiation, $\eta$ via long normal form
• Functional principles only from explicit equations ⇒ $57/70$ vs. $5/35$ on Benzmüller & Brown (2005)
• The missing rule $(\mathrm{ext})$ is identified

Parallelism is bottlenecked

• 8 workers: $3.27\times$ inference, but no more refutations ($680$ vs. $682$)
• Bottleneck is the single global closure search, not branch expansion ⇒ future work targets the architecture

Artefacts

• Four Hex packages (shot_ds, shot_un, shot_to, shot_tx) and the thesis as runnable Livebooks: github.com/jcschuster/shot-thesis

Backup

%ShotTx.Data.Parameters{} |> Kino.Tree.new

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

Outbox Pattern

---

Branches are data, and not independent workers like in Goéland (Cailler, 2022); this would explode the memory usage.

Workers pick up branches, apply a fixed number of steps to them, and return them to the working queue. Branches communicate their side-effects rather than apply them.

@type effect ::
        :no_effects
        | {:notify_ca, MapSet.t()}
        | {:record_provenance, [{Term.term_id(), Provenance.t()}]}
@type step_result ::
        {:continue, %__MODULE__{}, effect()}
        | {:split, my_branch :: %__MODULE__{}, sibling :: %__MODULE__{}}
        | {:instantiate, branches :: [%__MODULE__{}]}
        | {:idle, %__MODULE__{}}
        | {:saturated, {defs :: map(), literals :: MapSet.t()}}
        | {:exhausted, %__MODULE__{}}
        | {:closed, %__MODULE__{}}

Extensionality and Instance-based Methods in Tableau-based Higher-Order Automated Theorem Proving

---

BEAM Primitives Supporting Concurrent Theorem Proving

---

Supervision Trees

• A crashed process is automatically restarted according to some strategy. The VM is kept alive.
• Killing a supervisor instantly kills all its supervised processes.

⇒ Failure isolation and quick cancellation come for free.

Message Passing and Actor Model

• Every process has a mailbox
• call (synchronous) and cast (asynchronous)
• Publish-subscribe topics for broadcasting

Erlang Term Storage (ETS)

• global, concurrency-safe hash table
• useful as work queue for work-stealing processes
• can hold tombstones for work items (here: branches)

%ShotTx.Prover.Branch{} |> Kino.Tree.new

Kino.Mermaid.new """
sequenceDiagram
  participant C as Caller
  participant MG as Manager
  participant WQ as work_queue (ETS)
  participant W as Worker
  participant PS as branch_evidence PubSub
  participant CA as ContradictionAgent
  participant TS as Task.Supervisor

  C->>MG: prove(conjecture)
  MG->>WQ: seed root branch
  MG->>W: spawn N workers

  loop until closed / stalled / timeout
    W->>WQ: checkout branch
    Note over W: Branch.step/4 (pure)
    alt branch splits
      W->>WQ: push child branches
      W->>PS: broadcast {:branch_split, parent, children}
    else branch has closing options
      W->>PS: broadcast {:local_clashes, branch, options}
    else branch closes on ground contradiction
      W->>PS: broadcast {:branch_closed, branch}
    end
    PS-->>CA: deliver evidence
    CA->>TS: dispatch CSP (union of one option per open branch)
    Note over TS: ShotUn.unify(...) |> take(1)
    alt common unifier found
      TS-->>CA: {:ok, theta}
      CA->>MG: {:proof_result, {:unsat, theta}}
      MG-->>C: {:thm, proof}
    else no global unifier yet
      TS-->>CA: :error
      Note over CA: keep accumulating evidence
    end
  end

  Note over MG: workers all idle, trigger deepening
  MG->>W: {:wake_up, new_gamma, new_prim_depth}
"""