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