Abstract
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.
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.
| Original language | English |
|---|---|
| Pages | 19-20 |
| Number of pages | 2 |
| Publication status | Published - 20 Mar 2018 |
| Event | Automated Reasoning Workshop: ARW 2018 - University of Cambridge, Cambridge, United Kingdom Duration: 12 Apr 2018 → 13 Apr 2018 https://www.cl.cam.ac.uk/events/arw2018/arw2018-proc.pdf |
Conference
| Conference | Automated Reasoning Workshop |
|---|---|
| Country/Territory | United Kingdom |
| City | Cambridge |
| Period | 12/04/18 → 13/04/18 |
| Internet address |