Preface
⠀
UNIVERSITY OF BAMBERG
Applied Computer Science Degree Program in theFaculty of Information Systems and Applied Computer Sciences Master's Thesis 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 August 2026
Abstract
Tableau calculi for higher-order logic decompose a problem without clausifying it, at the cost of one global dependency: a free variable is rigid, so a value closing one branch commits every branch. This thesis presents Shot, a prover organised around that dependency. Every branch-level rule of its calculus over Church's simple type theory is binding-free, recording the condition under which a branch would close rather than choosing a value. Boolean extensionality is reached by renaming an opaque propositional argument onto the branch and instantiating it over the two truth values, the functional principles by expanding equalities at functional type, and the search rests on instance-based methods: general bindings, instance-based quantifier expansion, finite expansion of quantifiers over purely propositional types, and ordered demodulation under a term order stable under substitution. Closing the tableau is then a constraint satisfaction problem over the closure evidence of all open branches, solved by one process, while the branch expansion feeding it runs on a pool of BEAM workers over shared hash-consed terms. An untuned ablation over the TPTP higher-order corpus and a study on a structured problem set locate two limits: global closure produces about half of all refutations and does not receive the parallelism, so it is at present too weak for the architecture built around it, and the calculus decides most of the problems whose validity needs only conversion and Boolean extensionality and few of those where a functional principle is required, which locates a missing rule rather than a general weakness.
Keywords: Automated Theorem Proving $\cdot$ Higher-Order Logic $\cdot$ Semantic Tableaux $\cdot$ Parallel Proof Search
Acknowledgements
I thank Christoph Benzmüller and David Fuenmayor for the frequent and stimulating discussions during the preparation of this work. Their feedback and pointers to literature and concepts for higher-order proof search and adjacent topics was invaluable for both the design and the implementation of the calculus.
The Executable Record
The chapters of this thesis are Livebook notebooks and can be read as they stand or evaluated. Each cell stores the result it produced, so the argument can be followed without a runtime; the tables and diagrams that Kino draws are rebuilt by the front end and appear once the chapter has been evaluated. A typeset rendering of the same chapters, set for printing, is published beside the notebooks as shot-thesis.pdf.
