Download PDFOpen PDF in browser

A Combinator-Based Superposition Calculus for Higher-Order Logic (Technical Report)

EasyChair Preprint no. 3192

31 pagesDate: April 18, 2020

Abstract

We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggest that the method is competitive.

Keyphrases: combinatory, complete, higher-order, Superpsoition

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:3192,
  author = {Ahmed Bhayat and Giles Reger},
  title = {A Combinator-Based Superposition Calculus for Higher-Order Logic (Technical Report)},
  howpublished = {EasyChair Preprint no. 3192},

  year = {EasyChair, 2020}}
Download PDFOpen PDF in browser