Automated Theorem Proving in Higher-Order Logic

Abstract

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 higher-order automated theorem provers. Automated higher-order reasoning has long lagged behind its first-order counterpart. This is damaging since many proof assistants use higher-order logic as their core language. In this thesis, I explore methods of extending first-order theorem provers to support higher-order reasoning. My work involves reasoning about the combinatory calculus, a version of higher-order 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 first-order prover relatively easily. I have implemented the calculus in the leading first-order 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 higher-order 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)