Dear Daniel Schüssler and Koen Classen, I've tried using both logic-TPTP and the parser in the Equinox theroem prover. I wanted to list issues I had when I tried using the parsers. logic-TPTP http://hackage.haskell.org/package/logic-TPTP is implemented with alex and happy, and it is very close to the specification to the TPTP syntax when you look at the happy source file. So, I think it works very nice for the people who wants to work on source to source transformation from TPTP syntax. It also comes with pretty printer and exporting to plain text TPTP syntax. It seems to be tested against the TPTP problem set and also random testing with formulae generated from One problem I had with logic-TPTP parser is about dealing with comments. The TPTP syntax specification states that comments can come in between any tokens. Howerver, logic-TPTP assumes that it is only at the top level, and not in between the formlua. As a result, it fails to parse such formulae, for example, the following one: fof(equality_reflexive, axiom, ! [X] # for all X : X=X # X is equal to itself ). This is valid according to the TPTP syntax specification, and all the theorem provers I know (at least the ones in the TPTP world) accepts such formulae. I believe that there is a reason Daniel's logic-TPTP keeps the comment since TPTP syntax specification also states that comment is not to be processed same as whitespace in case theorem prover implementation may use the content of the comment as extra information. However, it is just not correct to reject valid formulae which contains comments inside. For a quick fix, I would suggest either (1) provide another set of parsing functions parse' and parseFile' that ignores all comment (2) export the lexer so that the user can build such versions of parsing functions themselves which ignores all comment tokens. (Maybe, in the long run, the happy syntax definition should allow comments between tokens?) In contrast, the parser in Equinox http://www.cs.chalmers.se/~koen/folkung/ can parse the formulae above. It just seem to ignore all comments since Equinox internally does not make use of any comments. However, the problem for me about the current parser implementation in Equinox is that it transforms the syntax tree into some normalized form. For example the formula ! [X,Y] : ... seem to be parsed as ! [X] : ! [Y] : ... So, when one wants to maintain the original form during the transformation the parser in Equinox would not be desirable for him. -- Ahn, Ki Yung