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
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.
- Easiest way: download the last release from here.
Uncompress the .tgz archive and read the included
- Anonymous (read-only) CVS access:
cvs -z3 -d:pserver:firstname.lastname@example.org:/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
cvs -z3 -d:ext:email@example.com:/cvsroot/athena-dpl co athena
There are two mailing lists:
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)
Copyright (c) 2005 - Alexandru Salcianu