Athena (Version 1.3)
Proof Central


Copyright (c) 1997-2012, Konstantine Arkoudas. All rights reserved.

This software is provided under the conditions set forth below. These conditions constitute a legal agreement and anyone downloading or using this software is bound by the terms of this agreement.

  1. Unlimited, non-exclusive, non-transferable, and royalty-free use of this software is permitted, provided that the licensee adheres to all the conditions set forth in this agreement. Failure on the part of the licensee to adhere to these conditions can result in revoking their rights to use this software. Redistribution of this software is permitted provided that any such redistribution retains and reproduces Athena’s copyright notice, disclaimers, and the list of conditions in this agreement.
  2. The Athena name and/or the names of its creator and/or the names of any people who have used Athena cannot be used to endorse or promote commercial products using Athena without explicit prior permission.
  3. Disassembly, decompilation, reverse-engineering, and any other modification of the Athena software is forbidden.
  4. The software is provided “as is” and without any support, updates, or maintenance. Nothing in this agreement shall require the licensor to provide licensee with support or fixes to any bug, failure, mis-performance, or other defect in the software. Any express or implied warranties, including, but not limited to, the implied warranties of merchantability and fitness for a particular purpose are disclaimed. In no event shall the licensor be liable for any direct, indirect, incidental, special, exemplary, or consequential damages (including, but not limited to, procurement of substitute goods or services; loss of use, data, or profits; or business interruption) however caused and on any theory of liability, whether in contract, strict liability, or tort (including negligence or otherwise) arising in any way out of the use of this software, even if advised of the possibility of such damage.
  5. The failure of the licensor to exercise or enforce any right or provision of this agreement shall not constitute a waiver of such right or provision.
  6. The licensor reserves the right to release the software under different license terms in the future or to stop providing the software at any time.

The licensor warrants that it owns Athena and has all rights necessary to grant the above license.

Downloading one of the distributions listed below indicates acceptance of this license.



Mac OS X


Microsoft Windows



To install Athena using any of the downloads (for Windows, we assume you have the Cygwin tools installed):

  1. Create an directory for Athena somewhere on your hard drive. Its name doesn’t matter.
  2. Create an environment variable ATHENA_HOME, whose value should be the path of the directory you created in step (1).
  3. Put the download file in the directory you created in step (1) and unpack it there. This will create lib (library) and util (utility) subdirectories and binary executable files athena, SPASS, and minisat. SPASS is an external ATP that can be invoked within Athena with the command spf, and minisat is a SAT solver that can be invoked within Athena with the procedure sat-solve. (For Windows, these binary files have extension .exe)

That’s it. To run the software, simply start a terminal, cd to the ATHENA_HOME directory, and type ./athena to start the program.


If the Mac athena halts with an error message about libgmp.10.dylib, you need to install the gmp (GNU Multiple Precision) package. It’s easily done with either homebrew
(brew install gmp) or macports (port install gmp).


Emacs users may prefer to run Athena from within Emacs in a *shell* or *compilation* window. See the util directory for an Emacs athena-mode for aid in editing Athena files, an athena-run shell script for batch execution of Athena files, and other tools.

Previous version

The previous version is available here.