Athena and ATPs

Athena is seamlessly integrated with state-of-the-art automated theorem provers (ATPs) such as Vampire, Spass, and E. These are often used to dispense with tedious reasoning steps, allowing the user to focus on the interesting parts of the proof. In Athena, an ATP invocation is just a method call, so the user can easily write code that calls the ATPs as frequently as necessary and with dynamically varying parameters. This is usually much more flexible and convenient than using ATPs in their normal batch-oriented mode from the command line (or with scripts).