Athena
This is the official web page for Athena, an interactive theorem proving
system developed by
Konstantine Arkoudas.
Overview
Athena is a programming language and an interactive theorem
proving environment rolled in one. As a programming language,
Athena is a higher-order functional language in the tradition
of Scheme and ML: strict and lexically scoped. It encourages
a programming style based on function calls and recursion,
but it also offers imperative features (e.g. ML-style updateable
memory cells) that can be used as an escape hatch
for the sake of efficiency.
As a theorem proving system, Athena is based on many-sorted
first-order logic. Many-sorted first-order logic is a very
expressive language; some logicians (e.g. Maria Manzano in
her "Extensions of first-order logic") have argued that
it can be viewed as a unifying framework
for all other logics, including higher-order logic.
It retains the tractability of first-order logic (completeness,
compactness, structural induction over terms and
formulas, efficient matching and unification algorithms, etc.),
while overcoming some of the modeling awkwardness of
single-sorted logic. Athena adds Hindley-Milner-style
polymorphism to many-sorted logic, which further increases
its flexibility.
As a logic tool, Athena can be used in four main capacities:
- For proof checking: Athena can be used as
a proof language,
i.e., a language in which to express and check proofs.
- For proof search: Athena can be used as
a
tactic language,
for writing provably sound theorem provers.
- As an high-bandwidth interface to cutting-edge
ATPs.
- As a
model finder.
More precisely---and succinctly---Athena is a type-omega
denotational proof
language (DPL) for a Fitch-style natural-deduction formulation of
polymorphic multi-sorted first-order logic.
Information related to Athena
- Athena
tutorial (Note: This tutorial is preliminary and incomplete; it does not
cover many aspects of the language, e.g., it does not explain how to
use Athena as a programming language. But it can get you up and running
on doing Athena proofs in a fairly short amount of time. Check here
frequently for updates.)
- Denotational Proof
Languages page: Athena is a member of a broad class of languages
called denotational proof languages (DPLs).
- Athena web site at
Rensselaer Polytechnic Institute (RPI)
Athena is used by Prof. David Musser in his Generic Algorithms
course at RPI. He has put together a site with some Athena
tutorials, an Emacs environment for Athena, and other useful resources.
- Some Athena problem sets from a DPL seminar that I ran at MIT a few
years ago:
Athena Applications
The following are some recent papers describing various applications
of Athena:
- Specification,
abduction, and proof
Konstantine Arkoudas
2nd
International Symposium on Automated Technology for Verification and
Analysis, National Taiwan University, October 2004 (ATVA 2004)
- Verifying
a File System Implementation
Konstantine Arkoudas, Karen Zee, Viktor
Kuncak, Martin Rinard
Sixth International Conference on Formal
Engineering Methods (ICFEM 2004)
-
Metareasoning for multi-agent epistemic logic
Konstantine Arkoudas,
Selmer Bringsjord
Fifth Workshop on Computational Logic in Multi-Agent
Systems (CLIMA V, 2004)
- Deductive
Runtime Verification
Konstantine Arkoudas, Martin Rinard
2004
Workshop on Runtime Verification (RV 2004)
- Integrating
model checking and theorem proving for relational reasoning
Konstantine
Arkoudas, Sarfraz Khurshid, Darko Marinov, Martin Rinard
7th
International Seminar on Relational Methods in Computer Science (RelMiCS
2003)
- Machine-Checkable
Correctness Proofs for Dataflow Analyses
Alexandru Salcianu,
Konstantine Arkoudas
Submitted for publication, December
2004
- A
trusted implementation of SLD-resolution
Konstantine Arkoudas
To be submitted for publication,
2005
Theses and dissertations using Athena
Some Masters theses and a recent PhD dissertation
that use Athena:
Download Athena
You can obtain a preliminary implementation of Athena here. For Windows
systems,
download the file
athenaWin32.zip and follow these
installation instructions .
For Linux, download
athenaLinux.tar.gz and consult these
installation instructions . Finally,
this is a distribution for Solaris machines (the installation
instructions are the same as for Linux) and
this is one for Mac machines.
Check here frequently for updates.
This is a preliminary page. If you have any questions or
suggestions, feel free to contact
Konstantine Arkoudas: konstantine "at sign" alum.mit.edu.