Automation for interactive proof: First prototype

Interactive theorem provers require too much effort from their users. We have been developing a system in which Isabelle users obtain automatic support from automatic theorem provers (ATPs) such as Vampire and SPASS. An ATP is invoked at suitable points in the interactive session, and any proof found is given to the user in a window displaying an Isar proof script. There are numerous differences between Isabelle (polymorphic higher-order logic with type classes, natural deduction rule format) and classical ATPs (first-order, untyped, and clause form). Many of these differences have been bridged, and a working prototype that uses background processes already provides much of the desired functionality.