Athena
This is a 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 awkardness of
single-sorted logic. Athena adds Hindley-Milner-style
polymorphism to many-sorted logic, which further increases
its flexibility.
As a logic framework, Athena can be used in several capacities:
- For proof representation and checking: Athena can be used as
a proof language,
i.e., a language in which to express and check proofs.
Athena proofs tend to be very compact (type annotations
are always omitted but can be automatically reconstructed)
and, for most important and common classes of problems,
they can be checked very efficiently (in time linear in
the size of the proof, in the worst case).
- For proof search: Athena can be used as
a
tactic language,
for writing provably sound theorem provers that exploit
domain-specific knowledge and heuristics to exceed
the efficiency of general-purpose ATPs.
- For specification and analysis: Athena can be
used to specify, simulate, and analyze a digital system.
Simulation is possible by virtue of the fact that specifications
in Athena are executable. If (possibly conditional) equations
are used for the specification, then they are executed using
Athena's native rewriting engine. If Horn clauses are used,
then execution is done by a seamless interface to efficient
Prolog engines (such as SWI
Prolog). If propositional or SMT logic is used for the
specification, then the spec can be executed and analyzed
via SAT or SMT solvers.
- As an high-bandwidth interface to cutting-edge
ATPs for first-order logic. Note that Athena automatically
translates its native polymorphic multi-sorted first-order logic
(possibly with subsorting) to the vanilla first-order logic
notation that such provers expect. Several heuristics are used
to make this translation efficient in practice.
- As an high-bandwidth interface to cutting-edge
SAT solvers and SMT solvers. Athena is seamlessly
integrated with various state-of-the-art SAT and SMT
solvers. By "seamlessly" we mean that the user never
leaves Athena's high-level notation: all the tedious
details of translating from Athena to the low-level
notations accepted by the solvers (and conversely, from
the low-level outputs of the solvers back to the high-level
notation of Athena) are handled under
the hood. Athena's translations to SAT and SMT are
finely tuned and highly efficient. Formulas with
millions of nodes are typically translated in a few seconds.
- As a
model finder for first-order logic.
- As a model checker. Athena is currently being integrated with SPIN.
This is done by (a) an embedding of Promela into Athena's programming
language; and (b) an Athena module encoding LTL (linear temporal
logic). This is work in progress.
Download Athena
You can obtain an older implementation as follows: Download
and uncompress the file
precomp-athena.tgz and consult the included README file.
Note that this implementation is quite outdated by now.
A new implementation is available as of March 2012 and can
be obtained by contacting me directly. It will be posted here
in the near future. The main changes from the old implementation:
- Infix syntax forms. While the old syntax (prefix,
s-expression-based) is still accepted, most Athena syntax
forms can now be expressed in infix.
- Modules: A "module" construct that is handly for managing namespaces.
- Subsorts. Athena now supports (possibly polymorphic) subsorts.
- A much richer library of primitives. Most notably, the
rewriting library now comes with a "chain" method that allows
for highly readable equational and implicational proofs.
(Both the idea for and the initial implementation of the equational
chain method are due to
David Musser.)
- The interfaces to the SAT and SMT solvers mentioned above,
the interface to Prolog, and the new translations from Athena's
native polymorphic multi-sorted subsorted first-order logic
to vanilla first-order logic (such as the TPTP format).
- A significantly more efficient overall implementation.
This is a preliminary page. If you have any suggestions, feel free to contact
Konstantine Arkoudas: konstantine "at sign" alum.mit.edu