logic-TPTP

For information about the TPTP format, see http://www.cs.miami.edu/~tptp/. 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.