Download PDFOpen PDF in browser

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

EasyChair Preprint 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: Superpsoition, combinatory, complete, higher-order

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 3192},
  year      = {EasyChair, 2020}}
Download PDFOpen PDF in browser