The Athena Interactive Theorem Prover

Athena is an interactive theorem prover for multi-sorted first-order logic with equality. For proof representation and checking, Athena uses a Fitch-style natural-deduction denotational proof language. You will have to read Kostas Arkoudas' PhD Thesis if you want to understand all these terms, but the intuitive idea is that Athena is designed to allow proofs expressed in a way that resembles paper-and-pencil proofs.

During a proof, Athena maintains an assumption base: the assumption base for a certain point in the proof contains all facts that are known to be true at that point. Primitive constructs (e.g., modus ponens) can add new facts to the assumption base. To prove an implication, Athena provides syntactic constructs that temporarily add the implication hypothesis to the assumption base during the scope of the proof for the implication conclusion.

Athena provides significant proof automation through user-defined methods in a Scheme-like Turing complete language, and through interfaces with external powerful automated theorem provers like Vampire and SPASS. Athena is also interfaced with paradox, a tool that processes first-order logic problems and tries to find finite-domain models for them.

Athena is released under the terms of the GNU GPL Licence.

A Little Bit of History

Athena was designed and implemented by Kostas Arkoudas during his PhD at MIT. In 2004, while doing some machine-checkable correctness proofs for dataflow analyses, Alex Salcianu added a few new features, packaged the Athena sources in a user-friendly way, and (biggest contribution!) convinced Kostas to release Athena under GNU GPL. We hope that other people will like Athena too and will contribute to this project.

Getting Started

Easiest way: download the last release from here. Uncompress the .tgz archive and read the included README.
Anonymous (read-only) CVS access:

cvs -z3 -d:pserver:anonymous@cvs.sourceforge.net:/cvsroot/athena-dpl co athena
Press Enter if prompted for a password.
Developer CVS access: First, you need to create an account on SourceForge and contact the project admin to obtain the right to edit the source. Next, you can start with the following commands:

export CVS_RSH=ssh cvs -z3 -d:ext:developername@cvs.sourceforge.net:/cvsroot/athena-dpl co athena

Mailing Lists

There are two mailing lists:

Athena users list: athena-dpl-users@lists.sourceforge.net Archives/Subscribe/Unsubscribe
Athena developers list: athena-dpl-devel@lists.sourceforge.net Archives/Subscribe/Unsubscribe

Tools That Athena Interfaces With

Athena is interfaced with the following highly-useful tools:

Vampire - A Theorem Prover for First-Order Classical Logic. (U. Manchester)
SPASS - An Automated Theorem Prover for First-Order Logic with Equality. (Max-Planck-Institut)
Paradox - A finite model finder for first-order logic. (U. Chalmers)

Hosted by