src/HOL/Tools/ATP/atp_problem.ML
Tue, 20 Mar 2012 18:42:45 +0100 blanchet removed obsolete temporary hack
Tue, 20 Mar 2012 18:42:45 +0100 blanchet tweaks
Tue, 20 Mar 2012 10:45:52 +0100 blanchet don't generate new SPASS constructs for old SPASS
Tue, 20 Mar 2012 00:44:30 +0100 blanchet continued implementation of term ordering attributes
Tue, 20 Mar 2012 00:44:30 +0100 blanchet internal renamings
Fri, 24 Feb 2012 11:23:35 +0100 blanchet added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
Thu, 09 Feb 2012 14:42:18 +0100 blanchet minor DFG fix
Thu, 09 Feb 2012 14:04:17 +0100 blanchet improved KBO weights -- beware of explicit applications
Thu, 09 Feb 2012 12:57:59 +0100 blanchet added possibility of generating KBO weights to DFG problems
Sat, 04 Feb 2012 12:08:18 +0100 blanchet improved hashing w.r.t. Mirabelle, to help debugging
Sat, 04 Feb 2012 12:08:18 +0100 blanchet tuned SPASS DFG output
Fri, 03 Feb 2012 18:00:55 +0100 blanchet extended SPASS/DFG output with ranks
Thu, 02 Feb 2012 01:55:17 +0100 blanchet tuning
Wed, 01 Feb 2012 17:16:55 +0100 blanchet really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
Tue, 31 Jan 2012 15:13:18 +0100 blanchet avoid name clash, really
Tue, 31 Jan 2012 15:10:03 +0100 blanchet fixed syntax bug in DFG output
Tue, 31 Jan 2012 14:39:21 +0100 blanchet new SPASS setup
Tue, 31 Jan 2012 12:43:48 +0100 blanchet distinguish between ":lr" and ":lt" (terminating) in DFG format
Tue, 31 Jan 2012 10:29:05 +0100 blanchet nicer keyword class avoidance scheme
Thu, 26 Jan 2012 20:49:54 +0100 blanchet better handling of individual type for DFG format (SPASS)
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file
Tue, 20 Dec 2011 18:59:50 +0100 blanchet don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
Tue, 20 Dec 2011 18:59:50 +0100 blanchet one more SPASS identifier
Tue, 13 Dec 2011 14:55:42 +0100 blanchet correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
Sat, 29 Oct 2011 13:15:58 +0200 blanchet always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added DFG unsorted support (like in the old days)
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added sorted DFG output for coming version of SPASS
Wed, 07 Sep 2011 13:50:17 +0200 blanchet fixed THF type constructor syntax
Tue, 06 Sep 2011 18:13:36 +0200 blanchet added dummy polymorphic THF system
Tue, 06 Sep 2011 09:11:08 +0200 blanchet tuning
Fri, 02 Sep 2011 14:43:20 +0200 blanchet use new syntax for Pi binder in TFF1 output
Wed, 31 Aug 2011 08:49:10 +0200 blanchet fixed explicit declaration of TFF1 types
Tue, 30 Aug 2011 16:07:46 +0200 blanchet generate properly typed TFF1 (PFF) problems in the presence of type class predicates
Tue, 30 Aug 2011 16:07:45 +0200 blanchet added type abstractions (for declaring polymorphic constants) to TFF syntax
Tue, 30 Aug 2011 16:07:45 +0200 blanchet implement more of the polymorphic simply typed format TFF(1)
Tue, 30 Aug 2011 16:07:34 +0200 blanchet first step towards polymorphic TFF + changed defaults for Vampire
Thu, 25 Aug 2011 23:38:09 +0200 blanchet make polymorphic encodings more complete
Thu, 25 Aug 2011 22:05:18 +0200 blanchet make TFF output less explicit where possible
Thu, 25 Aug 2011 13:55:52 +0100 nik added choice operator output for
Mon, 22 Aug 2011 15:02:45 +0200 blanchet tuning ATP problem output
Mon, 22 Aug 2011 15:02:45 +0200 blanchet clearer terminology
Wed, 17 Aug 2011 10:03:58 +0200 blanchet distinguish THF syntax with and without choice (Satallax vs. LEO-II)
Tue, 26 Jul 2011 14:53:00 +0200 blanchet further worked around LEO-II parser limitation, with eta-expansion
Tue, 26 Jul 2011 14:53:00 +0200 blanchet use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
Thu, 14 Jul 2011 16:50:05 +0200 blanchet added option to control which lambda translation to use (for experiments)
Thu, 14 Jul 2011 15:14:38 +0200 blanchet don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happy + tuning
Tue, 05 Jul 2011 17:09:59 +0100 nik improved translation of lambdas in THF
Tue, 05 Jul 2011 17:09:59 +0100 nik added generation of lambdas in THF
Tue, 05 Jul 2011 17:09:59 +0100 nik add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
Thu, 16 Jun 2011 13:50:35 +0200 blanchet added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users
Wed, 08 Jun 2011 16:20:19 +0200 blanchet pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
Tue, 07 Jun 2011 07:06:24 +0200 blanchet renamed ML function
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved ATP clausifier so it can deal with "x => (y <=> z)"
Mon, 06 Jun 2011 20:36:34 +0200 blanchet killed odd connectives
Wed, 01 Jun 2011 10:29:43 +0200 blanchet clausify "<=>" (needed for some type information)
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Fri, 27 May 2011 10:30:07 +0200 blanchet cleaner handling of equality and proxies (esp. for THF)
less more (0) -100 -60 tip