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

[ codec, library, math, theorem-provers ] [ Propose Tags ]

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.


Manual Flags


build test programs


Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info


Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


  • No Candidates
Versions [RSS] 0.1, 0.2.0,,,,,,,,,,,,,,,,,
Change log changelog.markdown
Dependencies ansi-wl-pprint (<1.0), array, base (>=4 && <5), bytestring, containers, logic-TPTP, mtl (<2.3), optparse-applicative (>=0.11 && <0.19), pcre-light, pointed, process, QuickCheck (>=2), semigroups, syb, transformers, transformers-compat (>=0.5) [details]
License LicenseRef-GPL
Author Daniel Schüssler
Maintainer Ahn, Ki Yung <kya@pdx.edu>, Daniel Schüssler <daniels@community.haskell.org>, Masahiro Sakai <masahiro.sakai@gmail.com>
Revised Revision 4 made by MasahiroSakai at 2023-06-11T14:24:07Z
Category Codec, Math, Theorem Provers
Bug tracker http://github.com/DanielSchuessler/logic-TPTP/issues
Source repo head: git clone http://github.com/DanielSchuessler/logic-TPTP.git
Uploaded by MasahiroSakai at 2020-02-28T12:17:14Z
Reverse Dependencies 1 direct, 0 indirect [details]
Executables ParseRandom, PrettyPrintFile, TestImportExportImportFile
Downloads 14570 total (36 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2020-02-28 [all 1 reports]