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

Mailing Lists

There are two mailing lists:

Tools That Athena Interfaces With

Athena is interfaced with the following highly-useful tools:
Hosted by Logo
Copyright (c) 2005 - Alexandru Salcianu