Add a --format argument to anthem translate

[teiesti]

It should be possible to specify the used formatter in anthem translate, e.g.

• anthem translate --with tau-star --format default
• anthem translate --with tau-star --format tptp
• anthem translate --with tau-star --format debug

[janheuer]

Following up on my prototype implementation (#154) with some thoughts on this issue.

There seem to be 2 different ideas what the format flag for translate should do:

1. just print out the same output as currently just formatted to be in tptp (see Zach's comment)
2. print current output formatted as tptp in the form of tff formulas and add preamble + helper axioms

1 of course makes sense in keeping it symmetric with the current output. I had some issues with this approach which is why I implemented the second approach:

• Without auxiliary axioms (i.e. transition axioms for gamma) the formulas are not correct. I think it would be better to output these and just have an optional --hide-auxilliary-axioms flag. (This applies to both a tptp format and also the current output.)
• The same argument of correctness can be made for outputting tptp without the preamble. Only with the preamble (and type definitions and some other helper axioms) does the tptp semantics match anthems semantics.
• Just having the tptp formatted formulas does not produce any usable tptp file.

This last issue leads to the bigger question of what the use case for using the tptp format is. My use case was my implementation of ordered completion:

• I have an implementation of the translate command but not any verification command that uses ordered completion.
• By having a format option that produces a valid tptp file I can then just manually add some conjecture to do some first trials with ordered completion.

I think this could generally be an interesting use case for when we have new translations. It would be possible to do some first test without having the possible extra efforts of implementing the verification (e.g. external equivalence verification adds a lot of complexity on top of the completion translation) and especially if the theory of the verification problem is not yet clear (e.g. the motivation for ordered completion was to get a replacement for normal completion in external equivalence, but it is not clear yet if this is actually possible from the theoretical side).