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.