Extending a High-Performance Prover to Higher-Order Logic
      Petar Vukmirović, Jasmin Blanchette, Stephan Schulz

Most users of proof assistants want more proof automation. Some proof
assistants discharge goals by translating them to first-order logic
and invoking an efficient prover on them, but much is lost in
translation. Instead, we propose to extend first-order provers with
native support for higher-order features. Building on our extension of
E to lambda-free higher-order logic, we extend E to full higher-order
logic. The result is the strongest prover on benchmarks exported from
a proof assistant.