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 FOF/TFF/TXF/THF
• Proofs by ATP systems, reconstructed by Metis
• Applications in the Archive of Formal Proofs

Application of ATP

• Supports some ATP systems locally (E, SPASS, Vampire, ...)
• Often uses RemoteSoT
• Problems added to the TPTP problem library

Isabelle is available online