This is a web page for Athena, an interactive theorem proving system developed by Konstantine Arkoudas.

- 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.

- 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