@hackage / logic-TPTP

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

Latest0.6.0.0

About

Metadata

  • Last updated , by MasahiroSakai
  • License LicenseRef-GPL
  • Categories Mathematics

  • Maintained by: Ahn, Ki Yung <kya@pdx.edu>, Daniel Schüssler <daniels@community.haskell.org>, Masahiro Sakai <masahiro.sakai@gmail.com>

  • Lottery factor: 1

Links

Installation

Tested Compilers

  1. 9.8.2
  2. 9.6.6
  3. 9.4.8
  4. 9.2.8
  5. 9.0.2
  6. 8.10.7
  7. 8.8.4
  8. 8.6.5

Package Flags

Use the -f option with cabal commands to enable flags

    buildtestprograms (off by default)

    build test programs

Readme

For information about the TPTP format, see https://www.tptp.org/.

Components:

  • 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.