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.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Arkoudas, Konstantine; Musser, David: Fundamental proof methods in computer science. A computer-based approach (2017)
- Ksystra, Katerina; Triantafyllou, Nikos; Stefaneas, Petros: On combining algebraic specifications with first-order logic via Athena (2017)
- Wang, Hongqiao; Lin, Guang; Li, Jinglai: Gaussian process surrogates for failure detection: a Bayesian experimental design approach (2016)
- Després, B.; Labourasse, E.: Angular momentum preserving cell-centered Lagrangian and Eulerian schemes on arbitrary grids (2015)
- Bard, Christopher M.; Dorelli, John C.: A simple GPU-accelerated two-dimensional MUSCL-Hancock solver for ideal magnetohydrodynamics (2014)
- Kunz, Matthew W.; Stone, James M.; Bai, Xue-Ning: \textitPegasus: a new hybrid-kinetic particle-in-cell code for astrophysical plasma dynamics (2014)
- Mignone, A.: High-order conservative reconstruction schemes for finite volume methods in cylindrical and spherical coordinates (2014)
- Lee, Dongwook: A solution accurate, efficient and stable unsplit staggered mesh scheme for three dimensional magnetohydrodynamics (2013)
- Ulbrich, Mattias; Geilmann, Ulrich; El Ghazi, Aboubakr Achraf; Taghdiri, Mana: A proof assistant for Alloy specifications (2012)
- Arkoudas, Konstantine: Specification, abduction, and proof (2004)