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

EasyChair Preprint 3192

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

@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}}