Format option for translate command #154
Conversation
There was a problem hiding this comment.
I saw a couple of typos (e.g. "prediates" instead of "predicates") but I have a more big-picture concern. I'm not sure it makes sense to include the standard preamble, types, transition axioms etc. as part of a format option for a first-order theory. This is adding semantic information to a syntactic operation. It also makes it asymmetric with the "default" option. Formatting an FOL theory should just format an FOL theory - I don't think it should mix instructions for a theorem prover into it. Since a tff statement in TPTP has the form tff(NAME, ROLE, FORMULA), all this format option should be doing is creating the FORMULA component.
|
Tobias also already mentioned a few issues with the code and also had a similar big picture concern. So I guess we should first discuss what the format option really should do. |
|
@janheuer You might want to raise an issue so that we can discuss how we can support your use case and come up with ideas for potential features. |
|
Seems like we already have an issue: #90! Oops... Sorry!" |
Adds a
--formatargument to the translate command with optionsdefaultandtptp. The TPTP output also includes the preamble and all the type definitions and so on. For the TPTP output it is also possible to change wich role the formulas are given with the--roleargument to eitheraxiomorconjecture.