Athena




Athena is a language and system for constructing and checking formal proofs. It was developed and continues to be evolved by K. Arkoudas as an example of what he calls ``Denotational Proof Languages,'' the subject of his PhD Dissertation (MIT, 2000). The official Athena Web site, where you can find a draft of an Athena tutorial, the current Athena distribution, and other helpful links, is
Athena.
Linux, Solaris, and Windows distributions are available for download.

Athena is installed on Rensselaer CSLab Solaris machines, which can be accessed remotely via SSH to solaris.remote.cs.rpi.edu. To use it, add the following lines to your .bashrc file: 
export ATHENA_HOME=/cs/musser/public.html/gsd/athena/system
export PATH=$PATH:$ATHENA_HOME
and in a (freshly started) bash shell enter the command 
athena
The above ATHENA_HOME definition points to a directory with an athena script that starts the appropriate version.

The most convenient way to interact with Athena is to create Athena expressions and deductions in an Emacs buffer and send them one by one to an Athena session running in an Emacs shell buffer. To facilitate this protocol, an Emacs macro and key-binding are defined in execute-in-shell.el. Either place the contents of this file directly in your .emacs startup file or add a command there to load it:

(load "/path/to/execute-in-shell")

For creating and editing Athena propositions, functions, and methods it's essential to have assistance with parenthesis balancing and proper indentation; this is provided by a special ``Athena mode'' for Emacs that you can set up by downloading athena-mode.el and adding the following lines to your .emacs file: 
(load "athena-mode")
(setq auto-mode-alist (cons '("\\.ath" . athena-mode) auto-mode-alist))
The first of these commands defines the mode and the second provides a trigger so that when any file with extension .ath is visited, Emacs automatically goes into Athena mode for editing that buffer.

Additional tutorial examples and some additional reference material on equational rewriting methods are presented in
David R. Musser and Aytekin Vargun, Proving Theorems with Athena. For replaying and experimenting with the proofs discussed in this document, download the source file, load it into Emacs, start Athena in an Emacs shell buffer, split the screen into two windows, one viewing the source file buffer and one viewing the shell buffer, and execute each Athena expression or deduction by placing the cursor within it and typing Control-/. This assumes you have defined execute-in-shell and bound it to Control-/ as recommended above. above.

You also need the file rewriting.ath containing proof methods based on the use of equations as rewriting rules and a method called conclude that aids in tracing proof executions.
Additional guidance for developing proofs with Athena can be found in:
David R. Musser, Heuristics for Proof Development in Athena.
Finally, for study of a much more extensive application of Athena, see Aytekin Vargun's Ph.D. thesis:
Aytekin Vargun, Code-Carrying Theory, Ph.D. thesis, Computer Science Department, Rensselaer Polytechnic Institute, 2006..

This document was translated from LATEX by HEVEA.