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