Higher-order Reasoning Vampire Style

    Research output: Contribution to conferenceAbstract


    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.
    Original languageEnglish
    Number of pages2
    Publication statusPublished - 20 Mar 2018
    EventAutomated Reasoning Workshop: ARW 2018 - University of Cambridge, Cambridge, United Kingdom
    Duration: 12 Apr 201813 Apr 2018


    ConferenceAutomated Reasoning Workshop
    Country/TerritoryUnited Kingdom
    Internet address


    Dive into the research topics of 'Higher-order Reasoning Vampire Style'. Together they form a unique fingerprint.

    Cite this