Higher-order Reasoning Vampire Style
Ahmed Bhayat, Giles Reger · Research Explorer (The University of Manchester) · 2018
Higher-order logic (HOL) is utilised in numerous domains from program verification to the formalisation of mathematics. However, automated reasoning in the higher-order domain lags behind first-order automation. Many higher-order automated provers translate portions of HOL problems to first-order logic (FOL) and pass them to FOL provers. However, FOL provers are not optimised for dealing with these translations. We extend the Vampire automated theorem prover with special inference rules to facilitate efficient reasoning with translated HOL problems. We present these inferences and explore preliminary results on their experimental performance compared to translations using axioms and to an automated HOL prover.