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.
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for alloy specifications (2012)
- Salcianu, Alexandru; Arkoudas, Konstantine: Machine-checkable correctness proofs for intra-procedural dataflow analyses. (2005)
- Arkoudas, Konstantine: Specification, abduction, and proof (2004)