Chapter 1: Introduction

Higher-Order Proof Search

Classical higher-order logic, in the form of Church's simple theory of types [Chu40] under Henkin's general model semantics [Hen50, And02], gains substantial expressiveness over first-order logic from a small extension of the syntax. Quantification over predicates and functions makes induction schemes, set-theoretic constructions, program semantics and the shallow embeddings of non-classical logics statable as single formulae rather than as first-order axiom schemes. The additional difficulty this creates for proof search has three independent sources.

The first is unification. Deciding whether two simply typed terms have a common instance is undecidable already at second order [Gol81], and Huet's pre-unification procedure [Hue75] replaces the decision with an enumeration that may be infinite and infinitely branching. Every calculus for higher-order logic therefore invokes an unbounded subprocedure from its most frequent operation, and every implementation has to bound that subprocedure somewhere and recover completeness by deepening. Decidable fragments exist (patterns [Mil91] most notably) and are worth detecting, but they do not cover the problems that motivate the logic.

The second is quantifier instantiation at predicate types. A witness for a variable of type $\bar{\tau}_n {\to} o$ is a formula, and no finite set of instances suffices in general. Andrews' primitive substitution [And89] enumerates approximations to such witnesses by their outermost logical symbol, which is a large branching factor added on top of an already unbounded one.

The third is extensionality. Henkin completeness demands rules for Boolean and functional extensionality, and what a calculus may assume about them is itself stratified into a hierarchy of model classes [BBK04]. Formulae occur as arguments, equality at function types is not decided by structure, and the ordinary first-order division of a problem into terms and formulae stops holding. Calculi differ in how much of this they build in. The principles can be supplied as axioms over the input, or as inference rules directed by the goal, which is the treatment developed for higher-order resolution in [BK98, Ben99a] and carried to equality and paramodulation in [Ben99b], with the alternatives compared in [Ben02].

The systems that address these difficulties are surveyed by Benzmüller and Miller [BM14] and are classified here by their calculus. TPS searches for expansion proofs by mating search [And81, Mil87, ABB00]. LEO-II uses extensional higher-order resolution, in which the extensionality principles are supplied as inference rules and unification constraints are carried as literals rather than solved on the spot [BK98, BPTF08, BSPT15]; Leo-III extends that line to extensional higher-order paramodulation [SB21]. Satallax and its reimplementation Lash use a ground tableau calculus with a SAT solver as the propositional decision procedure [Bro12, BK22]. Zipperposition and the higher-order modes of Vampire and E use superposition extended to $\lambda$-terms [BBT+21, VBB+21]. The competition record favours the last of these. In the THF division of CASC-J13, held at IJCAR 2026, the entrants were Vampire, Zipperposition, E, Leo-III and LEO-II; Vampire solved $354$ of $400$ problems and Zipperposition $347$, and no tableau-based system entered [Sut26].

Analytic Tableaux in Higher-Order Proving

A thesis that builds a higher-order tableau prover has to address that record, so the case against the method is stated first and without qualification. Satallax led higher-order proving through the 2010s and was then overtaken by superposition, by a wide margin and on the same benchmark set [VBB+21]. The reasons are structural rather than incidental. A saturation-based prover maintains a global clause set and a redundancy criterion, so every derived clause may simplify and subsume every other one; a tableau maintains a tree of branches, for which no comparable notion of one branch rendering another redundant is available. Free-variable tableaux are destructive, in that a closing substitution rewrites the whole tableau, so the standard proof procedure backtracks over instantiations and repeats work [Fit96, Hah01]. Equational reasoning, which superposition was designed around, has to be retrofitted. None of this is disputed here.

Four properties nevertheless argue for the method at higher order. The first of them is conceded by the superposition literature itself.

The input structure is preserved. Clausification is a lossy translation, and at higher order it is lossy in ways that first-order experience does not predict. Formulae occur inside terms, Boolean-typed arguments have to be lifted out, and an axiomatic encoding of the Boolean type degrades saturation performance measurably; the response has been to interleave clausification with the derivation instead of running it as a preprocessing step [NBTV21]. Vukmirović et al. put the comparison plainly: "One of the strengths of tableau provers is that they do not clausify the input problem", and "delaying the clausification through the use of calculus rules that act on formulas achieves the same effect in superposition" [VBB+21]. A tableau calculus obtains that property by construction. Its rules act in place on the connective at the root of a formula, so a subformula to which no rule has been applied is unchanged from the input. For a prover whose secondary aim is presentation, this property is relevant twice over.

The proof object is legible. A closed tableau is a tree whose nodes carry formulae in the vocabulary of the problem, and whose closure is witnessed by a pair of complementary literals and one substitution. It can be read without knowledge of the calculus, displayed as a tree, and verified by hand for small problems. Expansion proofs and matings offer a comparable representation [Mil87]. A refutation obtained by superposition after clausification, skolemisation, Boolean hoisting and simplification relates far less directly to the input formulae.

Rules compose additively. Higher-order tableau calculi have been extended by the addition of rules. Kohlhase's $\mathcal{HTE}$ added extensionality rules to a Smullyan-style base [Koh95, Smu68]; Konrad's HOT reworked that calculus for implementation [Kon98]; Backes and Brown added a choice operator, with completeness relative to Henkin models preserved [BB11]. Each addition is a case in a rule dispatch and a case in the corresponding soundness argument. The same is true of the additions made here: primitive substitution, ordered demodulation and the definition-unfolding and BDD preprocessing of Chapter 3 are separate rules with separate costs, each independently switchable, so that the ablation study of Chapter 8 can turn one off without disturbing the rest.

Failure is informative. A saturated branch that does not close is a candidate description of a model, which makes the method bidirectional: a failed proof attempt yields the material for a countermodel search. Satallax exploits this [Bro12], and external model finders accept the same material [BN10]. The model agent of Chapter 7 is based on it, and the third verdict this prover can return, that a branch is saturated but not decidably open, follows from treating the countermodel reading as a soundness obligation.

Against those four properties is one that is usually listed as a defect and is treated here as the central design constraint. The free variables introduced by $\gamma$-expansion are rigid: a variable denotes the same term on every branch it occurs on, and a closed tableau requires a single substitution closing all open branches simultaneously. Branch expansion is local, closure is global. In the standard proof procedure this global dependency is what forces backtracking, and it is why parallelising a tableau naively is unsound: two branches that each close under incompatible bindings have not closed the tableau.

The first-order literature already contains the reformulation that removes the backtracking. Giese's incremental closure keeps, for each branch, the set of substitutions that would close it, and searches for a common solution incrementally rather than committing to one instantiation and undoing it later [Gie01]. Read as an architecture rather than as a search strategy, this decomposes the tableau into many independent local computations and one shared constraint problem. The present work transfers that decomposition to higher order, where the local computations are more expensive, the constraints are pre-unifiers rather than unifiers [Hue75], and the enumeration underlying each constraint is unbounded. The deferral itself has a higher-order precedent on the resolution side, where unification constraints are carried as literals inside a clause and discharged only when a refutation depends on them [BK98, BPTF08]. The step taken here is to collect the deferred constraints of all open branches and solve them as one problem in a single process.

The claim made here is therefore not that tableaux outperform superposition on higher-order problems; the CASC record indicates otherwise and this thesis presents no evidence to the contrary. However, the tableau method admits a decomposition into independent local work and a single global constraint, which saturation-based calculi do not, since a clause set is shared by construction and mutual simplification makes every inference depend on every other [Bon00]. That decomposition has been exploited concurrently at first order and has not been exploited at higher order on a runtime designed for such computations. Whether doing so is profitable is an empirical question, addressed in Chapter 8.

Rigidity, Locality and Parallel Search

Parallel deduction has an established classification. Bonacina classifies strategies by granularity, by whether one process directs the others or the processes are peers, and by whether the parallelism subdivides a single search or runs several searches at once [Bon00]. In those terms the architecture of Chapter 6 is coarse-grained, peer-based, and a distributed search: branches are the unit of parallel work, no process directs another, and the search performed by a population of workers differs from the sequential search it derives from rather than reordering it.

Prior work that parallelises the tableau itself is represented by Goéland, which spawns a lightweight process per branch, communicates closing substitutions over channels, and reconciles them centrally [CRD+22]. Goéland is first-order, and the process-per-branch mapping it uses is the one design this thesis considered and did not adopt, for the reasons given in § The BEAM as Platform for Concurrency. A second line distributes the reasoning over a population of agents rather than parallelising the tableau, and it is the direct predecessor of the architecture built here.

Agent-Based and Cooperative Proof Search

Agent-based proof search begins with $\Omega$-Ants, where concurrent agents compute possible arguments for the inference rules applicable to the current partial proof and post them to a blackboard from which a proof planner selects [BS98, Sor01]. Its mature form, OANTS, arranges the agents in two layers over blackboards, admits external reasoning systems as agents alongside the internal ones, and is resource-adaptive: computation is reallocated between the agents according to what each has been observed to contribute, and agents that cannot contribute to the current goal are deactivated [BSJK08]. Konrad's HOT carries the blackboard into higher-order proving, running an extensional higher-order tableau calculus on a concurrent blackboard architecture [Kon98]; its concurrency serves the blackboard rather than branch expansion.

A second strand couples reasoners of different kinds. LEO-II is built as a cooperative prover: it performs extensional higher-order resolution itself and passes the essentially first-order part of a problem to an external first-order system, whose answer it integrates [BPTF08, BSPT15]. Whether such a pairing is worth its overhead, and what has to hold of the translation between the two logics for it to be, is examined directly in [BSJK05]; [WB16] asks the same question of agent populations in general. LeoPARD supplies the term data structures and the agent infrastructure on which the later systems of this line are implemented [WSB15]. The model agent of Chapter 7 belongs to this strand: it consults an external system about a single branch, and what differs is the direction of the question, satisfiability of a saturated branch rather than refutation of a subgoal.

Leo-III inherits from both strands. Its agent framework has a scheduler that collects the read and write sets of the tasks its agents propose and selects a maximal non-conflicting set of them by an approximation algorithm for combinatorial auctions [SWB16]. The framework has two modes, and the fine-grained one, in which each inference rule is an agent, was reported as "not competitive and still experimental"; the configuration Leo-III competes in runs a sequential loop inside a single agent, with parallelism confined to unification, redundancy checks and calls to external provers [BSW17, SB21]. That experience bears on the design question from one side: when every inference has to be arbitrated by a scheduler, the arbitration is the cost. The architecture of Chapter 6 arbitrates only closure, and leaves expansion unarbitrated.

Two things separate the design developed here from these systems. The first is the direction of control. No scheduler is advised by agents: workers expand branches and publish closure evidence; a single contradiction agent consumes that evidence and solves the global constraint; further agents subscribe to the same stream and may publish hints that a worker may ignore. An agent is added by subscribing and removed by not starting it, so each agent can be disabled without modifying the components that remain. The second is the level at which computation is allocated. OANTS allocates it between agents explicitly, on evidence of what each has contributed [BSJK08]. Here no component allocates it at all: preemption is counted in reductions by the runtime, and the worker pool is of fixed size, so what an agent receives is decided by the scheduler of the virtual machine rather than by the prover.

The BEAM as Platform for Concurrency

The choice of Elixir on the BEAM follows from the structure of the computation described above. The unit of parallel work is the branch, and the number of branches grows at every $\beta$-expansion, which suggests mapping each branch to its own process. That is not the design used here. Branches are created faster than they are closed, each retains its full formula set for as long as it lives, and each would publish closure evidence to a single contradiction agent whose mailbox and cartesian product both grow with the number of live branches. Memory consumption would then track the size of the tableau rather than the size of the pool, and the schedulers would be occupied by processes that are for the most part not running.

Branches are therefore values rather than processes. A branch is a data structure held in a public ETS table, and a fixed pool of long-lived worker processes takes branches from that table, applies a bounded number of rules to each, and returns them. The pool defaults to one worker per online scheduler, so the degree of parallelism follows the hardware while the number of branches in flight follows the problem. The runtime is used here for a work-stealing pool over shared structures that many processes read and write at once, rather than for a process per unit of work.

Four properties of the runtime are relevant [Arm03]. Scheduling is preemptive and reduction-counted, so a worker that has entered a long pre-unification enumeration cannot starve the workers that would have closed the tableau sooner; the bound on that enumeration is still needed for completeness, but it is no longer needed to keep the system responsive. Each process has its own heap, so garbage collection is per-process and collecting one worker does not suspend the others. Schedulers are per core, and the same program runs on one core and on many without a change in the code, so worker_pool_size sweeps a single implementation rather than comparing two in Chapter 8. ETS provides tables with per-slot read and write concurrency, which is what allows the branch queue, the traces, the provenance records and the published hints to be shared between workers without a coordinating process on the frequently executed path.

Message passing between isolated processes also enforces the calculus's central discipline through the primitives of the language rather than by convention. A worker cannot mutate another worker's state, since it holds no reference to it; the only shared mutable objects in a session are the ETS tables owned by a single process, and all global search state resides in them. Wherever the code accesses a shared table instead of sending a message, the local/global partition of Chapter 6 is apparent at the call site.

Supervision has a further consequence. A pre-unification stream that exhausts memory, or a rule application that raises on a malformed term, terminates one worker rather than the session; its supervisor restarts it and the remaining workers continue. The branch that worker held is not returned to the queue, since checkout removes it from the shared table, so the cost of a worker crash is one abandoned branch. Failure isolation therefore bounds the damage a single malformed term can do, and the defensive checks a single-process prover performs inline are replaced by process termination.

The disadvantages are stated with the same directness. The BEAM is not a fast substrate for the inner loops of a theorem prover. Term traversal, unification and order comparisons are allocation-intensive symbolic operations, and an OCaml or C implementation of the same algorithms performs more of them per second than an Elixir one; Satallax, Lash and Zipperposition are single-threaded systems with substantially better constant factors than are attainable here [Bro12, BK22, BBT+21]. Hash-consing of terms and ETS-resident caches reduce that difference, and the speedup from parallelism must compensate for the remainder. No part of this thesis assumes that it does.

It does not. On the structured set of higher-order problems of [BB05], the prover is about three times slower at the median than the fastest reference system on each problem it proves, and two orders of magnitude slower at the tail. A worker pool of one process per online scheduler multiplies inference by a factor of three over a single worker within the same budget and leaves the number of problems solved unchanged, because the parallelism reaches branch expansion rather than the global closure search that produces most of the refutations. Both measurements are reported in Chapter 8.

Two secondary considerations support the choice without being decisive for it. Elixir retains the developers who adopt it, ranking third among the most admired languages in the 2025 Stack Overflow developer survey behind Rust and Gleam [SO25], which is relevant for a research prototype intended to be read and extended by others. Its notebook environment, Livebook, is the medium of this thesis and is the subject of the next section.

Executable Presentation

Teaching and presentation are secondary aims of the Shot system, and they influenced the calculus only where no other property had to be given up. The prover's formatters print types and terms in the conventional annotated style rather than in the uncurried notation of Chapter 2, derivations are rendered as trees, and every rule carries a name a reader can look up. Since the tableau method was already the most readable of the candidate calculi, no substantial conflict between the two aims arose.

The thesis itself serves as the proof of concept for that aim. It is written as a set of Livebook notebooks [Liv25] following the principles of literate programming [Knu84]: the chapters are the source of truth, the LaTeX build reads them, and the executable cells run the prover being described. A rule classification, an enumeration of pre-unifiers, an orientation decision and a rendered proof object are computed when the chapter's cells are executed rather than asserted in prose. Three registers are kept typographically distinct throughout, as set out in Chapter 2, so that a claim about the mathematics and a claim about the implementation are never confused for one another.

The notebooks and a typeset rendering of them are archived under a single identifier, https://doi.org/10.5281/zenodo.22045933. A reader who follows a claim to the cell that settles it obtains the code and the stored outputs that produced the figures reported here. The identifier resolves to the version of the notebooks tagged v1.0, which is the version the printable document renders; later versions are separate entries in the same record.

Contributions

The thesis makes the following contributions.

• A higher-order free-variable tableau calculus over Church's simple type theory with primitive equality, extensional rules, primitive substitution, and equational reasoning by ordered demodulation, together with the preprocessing that precedes it (Chapter 3).
• A binding-free formulation of every branch-level rule. No rule commits to a value for a free variable; each records a closure condition as evidence. The consequences are traced through the equality rules, which admit only rewrites with an empty matcher, and through the term order, which must be stable under a substitution that has not yet been computed (Chapter 3, Chapter 5).
• A treatment of global closure as a constraint satisfaction problem over the closure evidence of all open branches, solved once by a dedicated process, giving a higher-order counterpart to incremental closure [Gie01] and removing backtracking over instantiations from the search (Chapter 6).
• A concurrent actor architecture realising that partition on the BEAM: a supervision tree per proof session, a fixed pool of worker processes stealing branches from a shared queue, shared state confined to tables owned by a single process, and closure evidence distributed by broadcast (Chapter 6). The measurements qualify the design: coverage is bounded by the rate at which global closure is attempted rather than by the rate at which branches are expanded, so enlarging the worker pool does not solve more problems at the budget measured (Chapter 8).
• Three peer agents built as consumers of that broadcast, for cross-branch instantiation hints, for satisfiability probing of saturated branches, and for global closure, each independently switchable; and reconstruction of an ordinary tableau proof from the derivation traces recorded by the concurrent search (Chapter 7).
• An orientation order for higher-order terms in $\eta$-long $\beta$-normal form, with the stability and typing properties the deferred-substitution discipline requires (Chapter 5).
• A set of concurrent data structures with explicit memory sharing, on which the pool design depends. Terms are hash-consed into a global pool, constructed once and thereafter referred to by identifier, so that a branch is cheap to write to a shared table and cheap for another worker to take from it; intermediate terms are built in process-local scratchpads and committed to the global pool only when a result survives, so that failed enumerations are discarded without adding to it. The session's search state is held in public ETS tables with read and write concurrency, addressed by branch prefix so that closure, tombstoning and hint lookup are single operations (Chapter 2, Chapter 6).
• The Shot ecosystem: four independently usable Hex packages, shot_ds (v1.3.1) for terms, types and the semantics of Church's simple type theory, shot_un (v0.2.1) for pre-unification, shot_to (v0.2.0) for the term order, and shot_tx (v0.1.0) for the calculus, the architecture and proof objects. Each carries its own documentation and test suite, and the first three are usable without the prover.
• An open-source implementation presented as executable notebooks in which the described behaviour is run rather than paraphrased.
• An ablation study over the agents, the calculus rules and the search control, with parameter sweeps and a scaling measurement over the worker pool, across the TPTP higher-order corpus (Chapter 8). Global closure through the contradiction agent accounts for about half of all refutations; iterative deepening, demodulation, finite $o$-quantification and atom decomposition contribute measurably; the suggestion agent, primitive substitution, instance-based $\gamma$-expansion and the size of the worker pool do not, at the budget measured.
• A qualitative evaluation on the structured set of [BB05] against five reference systems, characterising the coverage by the model class in which each problem is valid: $57$ of the $70$ problems valid without a functional principle are proved on every run, against five of the $35$ that require one (Chapter 8, worked example by example in Appendix A).

Scope and Non-Goals

The system is a research prototype and is not tuned for competition. No claim is made that it is faster than, or solves more problems than, any of the systems named above, and the evaluation is designed to measure the contribution of its own components rather than to place it in a ranking.

Soundness of the calculus is argued rule by rule, and the obligations are collected in § Soundness and Completeness of Chapter 3. Completeness is not established. That section states as a conjecture what a complete extension of the calculus would look like and names the rule the calculus lacks: the functional extensionality principles are reachable only from a formula that is already an equation, so the calculus as given is expected to be incomplete. The bounded pre-unification of Chapter 4 is recovered by iterative deepening, the interaction of demodulation with the extensionality rules is not analysed, and the semantic layering of [BBK04] is used to state what is assumed rather than to prove what is achieved.

The choice operator is not part of the calculus, so the fragment covered is narrower than that of [BB11]. Concurrency is confined to a single BEAM node; the runtime's distribution facilities are not used and multi-node scaling is left to future work. Integration with an interactive prover as a hammer-style backend is out of scope.

The logic reasoned about is monomorphic. Input is read in the TPTP typed higher-order dialects [Sut17, SB10], and rank-1 polymorphic TH1 problems [KSR16] are monomorphised during parsing, so a polymorphic symbol is presented to the calculus as a family of monomorphic ones. Problems whose proofs require an instance not produced by the monomorphisation are therefore not provable, and no reasoning about type variables takes place inside the calculus.

Outline

Notation and semantics are fixed in Chapter 2, which develops Church's simple theory of types with an uncurried, $\eta$-long $\beta$-normal presentation and Henkin general models, and defines the type-level vocabulary the later chapters depend on. The notational conventions follow those of Niederhauser and Middeldorp [NM26].

The calculus is given in Chapter 3: the tableau objects and their global and local states, the propositional and quantifier rules, primitive substitution, the extensionality rules for Boolean and functional equality, ordered demodulation, closure and discharge, literal processing, BDD-based preprocessing, the search bounds and the rule priorities that order the whole.

Two term-level chapters follow. Huet-style pre-unification, its three cases and the decidable fragments worth detecting are covered in Chapter 4. The orientation order used to gate rewriting, its parameters and the properties demanded of it by the deferred-substitution discipline are covered in Chapter 5.

The architecture is the subject of Chapter 6: the rigid variable problem and the local/global partition it forces, the supervision tree, the separation of pure branch logic from stateful shell, the evidence stream, global closure as constraint satisfaction, the message flow and iterative deepening. Its extensions, the two optional peer agents and proof reconstruction, are the subject of Chapter 7.

Measurements are reported in Chapter 8: the benchmark method and the scoring conventions, the baseline configuration, ablations of the agents, of the calculus rules and of the search control, scaling with the worker pool, the behaviour of the closure search under the two pool sizes, a second study on a structured problem set with the coverage it gives by model class, and threats to validity. Worked examples are collected in Appendix A, and Chapter 9 summarises, states the limitations that survive the evaluation, and sets out future work.

The principal findings, for a reader of this chapter alone: global closure through the contradiction agent is what the prover rests on, and removing it costs about half the refutations; the concurrent search multiplies inference without multiplying closure, so the worker pool reduces latency without extending coverage; and the calculus decides most of the problems whose validity needs only conversion and Boolean extensionality and few of those needing a functional principle, which locates the missing rule rather than a general weakness.

Chapter References

• [ABB00] Peter B. Andrews, Matthew Bishop, and Chad E. Brown. System description: TPS: A theorem proving system for type theory. In Automated Deduction (CADE-17), LNCS 1831, pages 164–169. Springer, 2000.
• [And02] Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, second edition. Applied Logic Series 27. Kluwer Academic Publishers, 2002.
• [And81] Peter B. Andrews. Theorem proving via general matings. Journal of the ACM, 28(2):193–214, 1981.
• [And89] Peter B. Andrews. On connections and higher-order logic. Journal of Automated Reasoning, 5(3):257–291, 1989.
• [Arm03] Joe Armstrong. Making Reliable Distributed Systems in the Presence of Software Errors. PhD thesis, Royal Institute of Technology (KTH), Stockholm, 2003.
• [BB05] Christoph Benzmüller and Chad E. Brown. A structured set of higher-order problems. In Theorem Proving in Higher Order Logics (TPHOLs 2005), LNCS 3603, pages 66–81. Springer, 2005.
• [BB11] Julian Backes and Chad E. Brown. Analytic tableaux for higher-order logic with choice. Journal of Automated Reasoning, 47(4):451–479, 2011.
• [BBK04] Christoph Benzmüller, Chad E. Brown, and Michael Kohlhase. Higher-order semantics and extensionality. The Journal of Symbolic Logic, 69(4):1027–1088, 2004.
• [BBT+21] Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Superposition with lambdas. Journal of Automated Reasoning, 65(7):893–940, 2021.
• [Ben02] Christoph Benzmüller. Comparing approaches to resolution based higher-order theorem proving. Synthese, 133(1–2):203–335, 2002.
• [Ben99a] Christoph Benzmüller. Equality and Extensionality in Automated Higher Order Theorem Proving. PhD thesis, Universität des Saarlandes, Saarbrücken, 1999.
• [Ben99b] Christoph Benzmüller. Extensional higher-order paramodulation and RUE-resolution. In Automated Deduction (CADE-16), LNCS 1632, pages 399–413. Springer, 1999.
• [BK22] Chad E. Brown and Cezary Kaliszyk. Lash 1.0 (system description). In Automated Reasoning (IJCAR 2022), LNCS 13385, pages 350–358. Springer, 2022.
• [BK98] Christoph Benzmüller and Michael Kohlhase. Extensional higher-order resolution. In Automated Deduction (CADE-15), LNCS 1421, pages 56–71. Springer, 1998.
• [BM14] Christoph Benzmüller and Dale Miller. Automation of higher-order logic. In Computational Logic, Handbook of the History of Logic 9, pages 215–254. Elsevier, 2014.
• [BN10] Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Interactive Theorem Proving (ITP 2010), LNCS 6172, pages 131–146. Springer, 2010.
• [Bon00] Maria Paola Bonacina. A taxonomy of parallel strategies for deduction. Annals of Mathematics and Artificial Intelligence, 29(1):223–257, 2000.
• [BPTF08] Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, and Arnaud Fietzke. LEO-II: A cooperative automatic theorem prover for classical higher-order logic (system description). In Automated Reasoning (IJCAR 2008), LNCS 5195, pages 162–170. Springer, 2008.
• [Bro12] Chad E. Brown. Satallax: An automatic higher-order prover. In Automated Reasoning (IJCAR 2012), LNCS 7364, pages 111–117. Springer, 2012.
• [BS98] Christoph Benzmüller and Volker Sorge. A blackboard architecture for guiding interactive proofs. In Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 1998), LNCS 1480, pages 102–114. Springer, 1998.
• [BSJK05] Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber. Can a higher-order and a first-order theorem prover cooperate? In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004), LNCS 3452, pages 415–431. Springer, 2005.
• [BSJK08] Christoph Benzmüller, Volker Sorge, Mateja Jamnik, and Manfred Kerber. Combined reasoning by automated cooperation. Journal of Applied Logic, 6(3):318–342, 2008.
• [BSPT15] Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, and Frank Theiss. The higher-order prover Leo-II. Journal of Automated Reasoning, 55(4):389–404, 2015.
• [BSW17] Christoph Benzmüller, Alexander Steen, and Max Wisniewski. Leo-III version 1.1 (system description). In LPAR-21 Workshops (IWIL), Kalpa Publications in Computing 1, pages 11–26, 2017.
• [Chu40] Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56–68, 1940.
• [CRD+22] Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, and Hinde Lilia Bouziane. Goéland: A concurrent tableau-based theorem prover (system description). In Automated Reasoning (IJCAR 2022), LNCS 13385, pages 359–368. Springer, 2022.
• [Fit96] Melvin Fitting. First-Order Logic and Automated Theorem Proving, second edition. Graduate Texts in Computer Science. Springer, 1996.
• [Gie01] Martin Giese. Incremental closure of free variable tableaux. In Automated Reasoning (IJCAR 2001), LNCS 2083, pages 545–560. Springer, 2001.
• [Gol81] Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13(2):225–230, 1981.
• [Hah01] Reiner Hähnle. Tableaux and related methods. In Handbook of Automated Reasoning, volume 1, chapter 3, pages 100–178. Elsevier and MIT Press, 2001.
• [Hen50] Leon Henkin. Completeness in the theory of types. The Journal of Symbolic Logic, 15(2):81–91, 1950.
• [Hue75] Gérard P. Huet. A unification algorithm for typed $\lambda$-calculus. Theoretical Computer Science, 1(1):27–57, 1975.
• [Knu84] Donald E. Knuth. Literate programming. The Computer Journal, 27(2):97–111, 1984.
• [Koh95] Michael Kohlhase. Higher-order tableaux. In Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1995), LNCS 918, pages 294–309. Springer, 1995.
• [Kon98] Karsten Konrad. HOT: A concurrent automated theorem prover based on higher-order tableaux. In Theorem Proving in Higher Order Logics (TPHOLs 1998), LNCS 1479, pages 245–261. Springer, 1998.
• [KSR16] Cezary Kaliszyk, Geoff Sutcliffe, and Florian Rabe. TH1: The TPTP typed higher-order form with rank-1 polymorphism. In Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), CEUR Workshop Proceedings 1635, pages 41–55, 2016.
• [Liv25] The Livebook Team. Livebook: Automate code and data workflows with interactive Elixir notebooks. https://livebook.dev, 2025.
• [Mil87] Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4):347–370, 1987.
• [Mil91] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
• [NBTV21] Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirović. Superposition with first-class Booleans and inprocessing clausification. In Automated Deduction (CADE-28), LNCS 12699, pages 378–395. Springer, 2021.
• [NM26] Johannes Niederhauser and Aart Middeldorp. Unification of deterministic higher-order patterns. In Automated Reasoning (IJCAR 2026), Lecture Notes in Computer Science. Springer, 2026. To appear; preprint arXiv:2601.14211.
• [SB10] Geoff Sutcliffe and Christoph Benzmüller. Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning, 3(1):1–27, 2010.
• [SB21] Alexander Steen and Christoph Benzmüller. Extensional higher-order paramodulation in Leo-III. Journal of Automated Reasoning, 65(6):775–807, 2021.
• [Smu68] Raymond M. Smullyan. First-Order Logic. Ergebnisse der Mathematik und ihrer Grenzgebiete 43. Springer, 1968.
• [SO25] Stack Overflow. 2025 Developer Survey: Technology. https://survey.stackoverflow.co/2025/technology, 2025.
• [Sor01] Volker Sorge. $\Omega$-ANTS: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Universität des Saarlandes, Saarbrücken, 2001.
• [Sut17] Geoff Sutcliffe. The TPTP problem library and associated infrastructure: From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017.
• [Sut26] Geoff Sutcliffe. The 13th IJCAR automated theorem proving system competition: CASC-J13. https://tptp.org/CASC/J13, 2026.
• [SWB16] Alexander Steen, Max Wisniewski, and Christoph Benzmüller. Agent-based HOL reasoning. In Mathematical Software (ICMS 2016), LNCS 9725, pages 75–81. Springer, 2016.
• [VBB+21] Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. In Automated Deduction (CADE-28), LNCS 12699, pages 415–432. Springer, 2021.
• [WB16] Max Wisniewski and Christoph Benzmüller. Is it reasonable to employ agents in automated theorem proving? In Agents and Artificial Intelligence (ICAART 2016), volume 1, pages 281–286. SCITEPRESS, 2016.
• [WSB15] Max Wisniewski, Alexander Steen, and Christoph Benzmüller. LeoPARD: A generic platform for the implementation of higher-order reasoners. In Intelligent Computer Mathematics (CICM 2015), LNCS 9150, pages 325–330. Springer, 2015.

Previous: Preface  $\cdot$  Contents  $\cdot$  Next: Chapter 2: Preliminaries