Implementation of Higher-Order Superposition

In the last decades, proof assistants have been immeasurably useful in formally proving validity of hard mathematical theories and correctness of safety-critical software. Using these tools one can formally describe a problem and produce machine-checkable proofs for statements about it. To make the checking phase efficient and trustworthy, proof steps need to be of fine granularity. As a consequence, seemingly simple statements must be proven in minute detail, making the use of proof assistants very tedious. In an attempt to automate significant parts of this proving process, assistants can invoke automatic theorem provers to finish the proof. However, most assistants are based on higher-order logic, while most automatic theorem provers are based on first-order logic. This means that the two systems must communicate through translations, which obfuscate the conjecture being proved and likely make proving the conjecture more difficult. In this thesis, we try to bridge this translation gap. We start from E, one of the best first-order proof assistants backends, based on the superposition calculus, and gradually extend it to higher-order logic. As this approach is large in scope, we split it into three parts. The first part extends E to support a fragment of higher-order logic devoid of lambda-abstraction, yielding a prover called Ehoh. Despite this extension being small in scope, Ehoh shows a stronger performance on proof assistant benchmarks than E. The second part concerns adding support for lambda-abstraction. The most important challenge we faced during this extension is that of higher-order unification. At the time we started, the state-of-the-art procedure for full higher-order unification was the one developed in 1970s. We designed a new procedure inspired by this one that enumerates fewer redundant unifiers, has many modern optimizations built in, and can easily be customized to trade its completeness for performance. It is implemented in a prototype prover called Zipperposition, a less efficient but more easily extendible prover compared to E. Our evaluation shows that our procedure substantially improves on the state of the art. The last part concerns adding native support for Boolean terms. For this part we took inspiration from traditional automatic higher-order provers, based on tableaux. We fitted those techniques in the superposition context and implemented them in Zipperposition. They made Zipperposition the best prover in the higher-order division of the annual CASC theorem prover competition for two consecutive years. After testing out our ideas in Zipperposition, we decided to go back to Ehoh and extend it to full higher-order logic, obtaining a prover called lambda E. We chose the most successful approaches implemented in Zipperposition that can be ported easily to lambda E. The results were once again positive: Our evaluation shows that lambda E is the best prover on proof assistant benchmarks, and second only to Zipperposition on a standard benchmark set. We took our idea of porting techniques from weaker to stronger logics one step back: We explored SAT simplification techniques that can be implemented in the superposition context. We discovered that while some of them can be used during proving, most of them work best as preprocessors. In conclusion, the work described in this thesis shows that first- and higher-order provers are much more alike than previously thought. Furthermore, we showed that through carefully designed and tuned extension, a first-order prover can become an award-winning higher-order prover.