Athena as a proof language
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.