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:
  1. 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).

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

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

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

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

  6. As a model finder for first-order logic.

  7. 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:
  1. Infix syntax forms. While the old syntax (prefix, s-expression-based) is still accepted, most Athena syntax forms can now be expressed in infix.

  2. Modules: A "module" construct that is handly for managing namespaces.

  3. Subsorts. Athena now supports (possibly polymorphic) subsorts.

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

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

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