A Lambda-Superposition Tactic for Isabelle/HOL

Abstract

This paper introduces slam, an Isabelle/HOL tactic and automated theorem prover based on the λ-superposition calculus. An alternative to Isabelle’s metis tactic, slam targets higher-order logic directly, avoiding the overhead introduced by metis’s translations to first-order logic. Like metis, slam can be used as a Sledgehammer backend to reconstruct proofs produced by external higher-order automated theorem provers such as E, Vampire, and Zipperposition.