Set of support for higher-order reasoning

Research output: Contribution to journalConference articlepeer-review

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. One of the reasons for this is that the axioms introduced during the translation (e.g. those defining combinators) may combine with each other during proof search, deriving consequences of the axioms irrelevant to the goal. In this work we evaluate the extent to which this issue affects proof search and introduce heuristics based on the set-of-support strategy for minimising the effects. Our experiments are carried out within the Vampire theorem prover and show that limiting how axioms introduced during translation can improve proof search with higher-order problems.

Original languageEnglish
Pages (from-to)2-16
Number of pages15
JournalCEUR Workshop Proceedings
Volume2162
Publication statusPublished - 1 Jan 2018
Event6th Workshop on Practical Aspects of Automated Reasoning, PAAR 2018 - Oxford, United Kingdom
Duration: 19 Jul 2018 → …

Fingerprint

Dive into the research topics of 'Set of support for higher-order reasoning'. Together they form a unique fingerprint.

Cite this