Import, export etc. for TPTP, a syntax for first-order logic

Latest on Hackage:

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

GPL licensed by Daniel Schüssler
Maintained by Ahn, Ki Yung, Daniel Schüssler

For information about the TPTP format, see http://www.cs.miami.edu/~tptp/.


  • Parser (parse)

  • Exporter (toTPTP)

  • Pretty-printer (pretty)

  • QuickCheck instances (generation of random formulae)

  • diff : Get a "formula" which represents the differences between two given formulae (equal subexpressions are truncated; so are the subexpressions of subexpressions whose heads already differ)

Tests passed:

  • For randomly generated formulae, parse . toTPTP == id

  • For all files in the TPTP (v 5.2.0) distribution's Problems subtree which don't match the regex "^(thf|tff)(", parse . toTPTP . parse == parse

Not yet implemented: The new thf and tff formula types.


  • Fix compilation error with containers >=0.5.8 (Thanks to @msakai)

  • Fix compilation error with transformers >=0.5.1 and GHC <7.10 (Thanks to @msakai)

  • GHC 7.10.1 compatibility (Thanks to @agomezl)

  • For transformers <, use the Eq/Ord/Show/Read Data.Functor.Identity orphan instances from transformers-compat instead of defining our own
comments powered byDisqus