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.
© 2012 Konstantine Arkoudas Contact Me