Add Comorphism from CASL to TPTP (#1731) * adapted SuleCFOL2SoftFOL to SuleCFOL2TPTP * SuleCFOL2TPTP: made it compile * removed superfluous stuff from comorphism * description of comorphism * Add implementation notes. * Add first functions structure, implement subsort encoding. * Implement remainder of sort axioms and function axioms. * Work in progress: prepare sign. * Handle overloading of ops and preds. * Resolve conditionals and translate formulae. * Rename variables (must start uppercase). * Remove translation clutter. * Rename target logic. * Create translated Sign. * Fix resolving unique existential quantifier. * Fix resolving Conditional TERMs. * Lots of small fixes. * More small fixes. * Work in progress: Recognise conjectures. * Work in progress: Recognise conjectures #2. * Ensure that the tempdir exists. * Fix sentence name translation. * Work on TODOs. * Fix subsort sentences. * CASL test file for comorphisms * more CASL tests * Replace own code be CASL.Utils code. * more CASL tests * more CASL tests * corrected sublogic * Nat example * Replace all non-alphanumeric characters. * Move Morphism to Morphism.hs and rename TPTP.Logic to TPTP.Logic_TPTP. * Remove now useless comments. * use scoped type variables * Remove sentence prefix. * Add helper functions for 'and' and 'or'. * Translate false to false. * Fail with the module name in the message. * Add reference to Hets issue. * Translate space to underscore. * Fix partial overloading translation. * Get rid of compiler warnings. * Simplify language_name. * Fix error message. * Simplify GenSuleCFOL2TPTP data structure.

Complete TPTP support (#1707) * Add option to print the AST in XML/JSON output. Turn it off by default. * Add abstract syntax of TPTP. * Add parens and brackets to Common.Lexer. * Add TPTP Parser. * Add TPTP Sign. * Add TPTP Morphism. * Add TPTP StaticAnalysis. * Fix IRI character parsing. * Add TPTP Pretty. * Add TPTP Logic. * Map the tptp and p file extension to the TPTP logic for input. * Add LibDefn parser for TPTP. * Write TPTP output. * Add EProver to TPTP. * Add TPTP Sublogics. * Add SPASS prover to TPTP. * Add Vampire prover to TPTP. * Add Darwin prover to TPTP. * Add Leo-II prover to TPTP. * Add Geo-III prover to TPTP - It does not support a timeout. * Add CVC4 prover to TPTP. * Add Isabelle prover to TPTP. * Make IRI compatible with TPTP library file names. * Revert "fail if names of sentences appear as names of symbols #1630" This is a combination of 3 commits: * Revert "check that the Result has no errors" This reverts commit 9542b929f3cfabf1491c3f0489acf92ba703968f. * Revert "better error message" This reverts commit a7ea46d4c76b11735234092d0a50efcbc56f9642. * Revert "fail if names of sentences appear as names of symbols" This reverts commit 2487bae09bf3aabc7085880aee616648fe5ca241. * Fix usage of magic file There were other (system) magic files invoked as well with a higher priority. Using the MAGIC environment variable instead of the argument --magic-file overrides this behaviour and only uses the specified magic file. * Fix magic file The escaping of "@" and "(" is not needed. The escaping of a trailing space in clif is needed. * Add TPTP to magic file. * Add Satallax prover to TPTP. * Properly check for http[s] URIs. * Allow file:// in libdirs. * Allow only one http[s] libdir - Parse the port correctly. * Fix all remaining parsing problems. * Move functions to debug the parser to a separate module. * Get rid of all TPTP related compiler warnings. * Move the type 'Morphism' to 'TPTP.Morphism'. * Rename: TPTP/Logic.hs -> TPTP/Logic_TPTP.hs * Implement all_sublogics. * Recognise negated_conjecture as a proof obligation.