First order formula parsers in Haskell (logic-TPTP and the one in Equinox)
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:
! [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
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.