Superposition with Lambdas

Bentkamp, A; Blanchette, J; Tourret, S; Vukmirovic, P; Waldmann, U

Bentkamp, A (corresponding author), Vrije Univ Amsterdam, Dept Comp Sci, Sect Theoret Comp Sci, De Boelelaan 1111, NL-1081 HV Amsterdam, Netherlands.

JOURNAL OF AUTOMATED REASONING, 2021; 65 (7): 893

Abstract

We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but exclud......

Full Text Link