A Combinator-Based Superposition Calculus for Higher-Order Logic

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


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.

Original languageEnglish
Title of host publicationAutomated Reasoning
PublisherSpringer Nature
ISBN (Electronic)978-3-030-51074-9
ISBN (Print)978-3-030-51073-2
Publication statusPublished - 4 Jul 2020

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'A Combinator-Based Superposition Calculus for Higher-Order Logic'. Together they form a unique fingerprint.

Cite this