History log of /hets/TPTP/Prover/Isabelle.hs
Revision Date Author Comments Expand
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7f 22-Aug-2017 Eugen Kuksa <kuksa.eugen@gmail.com>

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.

/hets/.gitignore /hets/Common/DebugParser.hs /hets/Common/FileType.hs /hets/Common/IRI.hs /hets/Common/Id.hs /hets/Common/Lexer.hs /hets/Common/Utils.hs /hets/CommonLogic/Lexer_CLIF.hs /hets/Comorphisms/LogicList.hs /hets/CspCASL/Parse_CspCASL_Process.hs /hets/Driver/Options.hs /hets/Driver/ReadFn.hs /hets/Driver/ReadLibDefn.hs /hets/Driver/WriteFn.hs /hets/Hets.cabal /hets/Logic/Logic.hs /hets/Makefile /hets/PGIP/Output/Proof.hs /hets/PGIP/Server.hs /hets/SoftFOL/DFGParser.hs /hets/Static/AnalysisStructured.hs /hets/Static/ToJson.hs /hets/Static/ToXml.hs /hets/TPTP/AS.der.hs /hets/TPTP/Common.hs /hets/TPTP/Documents/TPTPSyntax.html /hets/TPTP/Logic_TPTP.hs /hets/TPTP/Morphism.hs /hets/TPTP/Morphism/Sentence.hs /hets/TPTP/ParseAsLibDefn.hs /hets/TPTP/Parser.hs /hets/TPTP/Pretty.hs CVC4.hs Common.hs Darwin.hs EProver.hs EProver/ProofParser.hs Geo3.hs Isabelle.hs Leo2.hs ProofParser.hs ProverState.hs SPASS.hs SPASS/ProofParser.hs Satallax.hs Vampire.hs Vampire/ProofParser.hs /hets/TPTP/Sign.hs /hets/TPTP/StaticAnalysis.hs /hets/TPTP/Sublogic.hs /hets/magic/hets.magic