Proof Central: Athena

Athena

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.

The User’s Guide and Reference are Chapter 2 and Appendix A of Fundamental Proof Methods in Computer Science, respectively.

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).
The primary objectives in the design of Athena were proof readability and writability. The goal is to allow for structured, high-level proofs expressed in roughly the same style and at the same level of abstraction as the informal proofs that computer scientists and mathematicians write in practice. To that end, Athena uses a Fitch style of natural deduction instead of the more customary sequent systems or proof trees. Fitch-style natural deduction is formalized by means of novel block-structured syntactic constructs and so-called assumption-base semantics.
For proof search: Athena can be used as a tactic language, or writing provably sound theorem provers that exploit domain-specific knowledge and heuristics to exceed the efficiency of general-purpose ATPs.
An Athena proof can easily be abstracted and turned into a proof algorithm that can be applied to different arguments. Such proof algorithms are called methods. Methods are guaranteed to produce sound results. More precisely, if a method ever produces a conclusion P, we can be assured that P is a logical consequence of the assumption base in which the method was applied. In Athena, a Fitch style of natural deduction is used not only for writing proofs but also for writing methods. In our experience, this makes methods much easier to write, in the same way (and for the same reasons) that writing proofs in Fitch-style systems is considered to be much easier than writing proofs in sequent systems or in proof-tree formats.
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. If propositional or SMT logic is used for the specification, then the spec can be executed and analyzed via SAT or SMT solvers.
As a high-bandwidth interface to cutting-edge ATPs for first-order logic: Athena is seamlessly integrated with state-of-the-art automated theorem provers (ATPs) such as Vampire, Spass, and E. These are often used to dispense with tedious reasoning steps, allowing the user to focus on the interesting parts of the proof. In Athena, an ATP invocation is just a method call, so the user can easily write code that calls the ATPs as frequently as necessary and with dynamically varying parameters. This is usually much more flexible and convenient than using ATPs in their normal batch-oriented mode from the command line (or with scripts).
Note that Athena can automatically translate 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 a 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: Athena is also integrated with model generators.
Model generation is useful for consistency checking, and in particular for falsifying conjectures: If we are not sure whether a formula follows from a given set of premises (e.g., suppose that an ATP cannot show this, and we cannot think of a proof ourselves), we can try to find a counter-model, i.e., a model in which all the premises are true but the formula in question is false. Model generators can be used to find such models automatically.

Athena source code and binaries (for Windows, Mac OS, and Linux) are available on GitHub, hosted by the Athena Foundation. Although Athena is undergoing further development on GitHub, access to Athena version 1.4.1 (FPMICS), which works with all of the book’s examples and exercises, will be retained there.