The Sledgehammer in Isabelle

About the Sledgehammer in Isabelle

• Finds proofs in higher-order logic
• Axioms selected from background theory
• Axioms and conjecture translated to FOL
• Calls first-order ATP systems
• Proofs verified by reconstruction with Metis

Application of ATP

• Supports E and SPASS locally
• Can also use RemoteSoT (mostly for Vampire)
• Problems added to the TPTP problem library
• RemoteSoT avoids need for local installation of ATP systems

Isabelle is available online