 To help prove higher-order theorems and discharge goals arising in interactive proofs, the user can ask Isabelle/HOL to invoke external first-order provers through Sledgehammer (Paulson 2010), a subsystem aimed at combining the complementary capabilities of automated reasoning systems of different types, including SMT solvers (see 4.2 SAT Solvers, in this article; Blanchette et al. 2013). LEO-II (Benzmüller et al. 2015) is also a resolution-based automated theorem prover for higher-order logic that has been applied in a wide array of problems, most notably in the automation of Gödel’s ontological proof of God’s existence (see 4.6 Logic and Philosophy, in this article). 