Proof assistants are rapidly gaining in importance and traction. Due to the complexity of modern mathematics, a number of mathematicians have advocated the use of proof assistants, most famously field medalist Vladimir Voevodsky. There are currently projects underway to encourage collaboration between mathematicians and proof assistant designers such as the Lean Forward project. However, one of the largest stumbling blocks to the uptake of proof assistants is their lack of automation. A single line of a pen and paper proof can translate to many lines of a formal proof. A major weakness in existing automation is the absence of strong higherorder automated theorem provers. Automated higherorder reasoning has long lagged behind its firstorder counterpart. This is damaging since many proof assistants use higherorder logic as their core language. In this thesis, I explore methods of extending firstorder theorem provers to support higherorder reasoning. My work involves reasoning about the combinatory calculus, a version of higherorder logic that does not utilise binders. I present a novel term ordering for combinatory terms that orients all combinator axioms left to right. I then use this ordering to parameterise a modified version of the superposition calculus. I prove the calculus to be sound and complete for the clausal (Boolean free) fragment of combinatory logic. Due to the absence of binders in combinatory logic, the calculus I have developed can be implemented in a firstorder prover relatively easily. I have implemented the calculus in the leading firstorder theorem prover Vampire. I discuss the implementation and describe the modifications required to Vampire's data structures and algorithms. Vampire's performance as compared with other leading higherorder provers displays promise.
Date of Award  1 Aug 2021 

Original language  English 

Awarding Institution   The University of Manchester


Supervisor  Peter Lammich (Supervisor) & Giles Reger (Supervisor) 

 Formal logic
 Superposition
 Computer proofs
 Automated theorem proving
 Higherorder logic
 Vampire
Automated Theorem Proving in HigherOrder Logic
Bhayat, A. (Author). 1 Aug 2021
Student thesis: Phd