src/HOL/TPTP/atp_problem_import.ML
Wed, 06 Jun 2012 10:35:05 +0200 blanchet add missing timeout multiplier
Wed, 06 Jun 2012 10:35:05 +0200 blanchet renamed TPTP commands to agree with Sutcliffe's terminology
Wed, 06 Jun 2012 10:35:05 +0200 blanchet don't use aggressive with HO ATP
Thu, 24 May 2012 18:21:54 +0200 blanchet make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
Tue, 22 May 2012 16:59:27 +0200 blanchet compile
Mon, 21 May 2012 10:39:32 +0200 blanchet add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
Mon, 30 Apr 2012 21:59:10 +0200 blanchet export more symbols
Sun, 29 Apr 2012 11:44:33 +0200 blanchet split into demo and competitive version
Fri, 27 Apr 2012 22:36:27 +0200 blanchet use Nitpick as an oracle for finite problems
Fri, 27 Apr 2012 22:36:27 +0200 blanchet add extensionality to first-order provers
Fri, 27 Apr 2012 15:24:37 +0200 blanchet thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
Fri, 27 Apr 2012 15:24:37 +0200 blanchet move LEO-II closer to the top, for testing
Fri, 27 Apr 2012 15:24:37 +0200 blanchet smaller batches, to play safe
Fri, 27 Apr 2012 13:19:21 +0200 blanchet tuning
Fri, 27 Apr 2012 12:16:10 +0200 blanchet more tweaking of TPTP/CASC setup
Thu, 26 Apr 2012 01:05:06 +0200 blanchet further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
Thu, 26 Apr 2012 00:28:06 +0200 blanchet tuning; no need for relevance filter
Wed, 25 Apr 2012 22:00:33 +0200 blanchet more work on TPTP Isabelle and Sledgehammer tactics
Wed, 25 Apr 2012 22:00:33 +0200 blanchet more work on CASC setup
Wed, 25 Apr 2012 14:33:21 +0200 blanchet tweak TPTP Nitpick's output
Tue, 24 Apr 2012 09:47:40 +0200 blanchet smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
Tue, 24 Apr 2012 09:47:40 +0200 blanchet handle TPTP definitions as definitions in Nitpick rather than as axioms
Tue, 24 Apr 2012 09:47:40 +0200 blanchet get rid of old parser, hopefully for good
Sun, 22 Apr 2012 14:16:46 +0200 blanchet added timeout argument to TPTP tools
Sat, 21 Apr 2012 11:15:49 +0200 blanchet prepend PWD to relative paths
Sat, 21 Apr 2012 11:15:49 +0200 blanchet reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
Wed, 18 Apr 2012 23:13:11 +0200 blanchet remove old TPTP CNF/FOF parser; always use Nik's new parser
Wed, 18 Apr 2012 22:40:25 +0200 blanchet tuned SZS status output
Wed, 18 Apr 2012 22:16:05 +0200 blanchet started integrating Nik's parser into TPTP command-line tools
Mon, 23 Jan 2012 17:40:32 +0100 blanchet implemented "tptp_refute" tool
Mon, 23 Jan 2012 17:40:32 +0100 blanchet added problem importer
less more (0) tip