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).