Higher-order Reasoning Vampire Style

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