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.
- 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.
- 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.
- Disassembly, decompilation, reverse-engineering, and any
other modification of the Athena software is forbidden.
- 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.
- 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.
- 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
To install Athena using any of the downloads (for Windows, we
assume you have the Cygwin tools installed):
- Create an directory for Athena somewhere on your hard drive. Its
name doesn’t matter.
- Create an environment variable ATHENA_HOME, whose value
should be the path of the directory you created in step (1).
- 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
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.
The previous version is available here.