| Thu, 24 Jul 2014 00:24:00 +0200 |
stick to external proofs when invoking E, because they are more detailed and do not merge steps
|
file | diff | annotate |
| Sat, 12 Jul 2014 11:31:23 +0200 |
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
|
file | diff | annotate |
| Tue, 24 Jun 2014 08:19:57 +0200 |
added 'dummy_thf_ml' prover for experiments with HOLyHammer
|
file | diff | annotate |
| Tue, 17 Jun 2014 16:02:49 +0200 |
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
|
file | diff | annotate |
| Mon, 16 Jun 2014 19:41:01 +0200 |
use right delimiters for Waldmeister proofs
|
file | diff | annotate |
| Mon, 16 Jun 2014 19:41:00 +0200 |
added 'waldmeister_new' as ATP
|
file | diff | annotate |
| Mon, 16 Jun 2014 19:40:04 +0200 |
moved code around
|
file | diff | annotate |
| Mon, 16 Jun 2014 19:39:41 +0200 |
give Z3 TPTP proofs a chance
|
file | diff | annotate |
| Mon, 16 Jun 2014 16:18:15 +0200 |
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
|
file | diff | annotate |
| Mon, 02 Jun 2014 15:10:18 +0200 |
basic setup for zipperposition prover
|
file | diff | annotate |
| Mon, 19 May 2014 23:43:53 +0200 |
use E 1.8's auto scheduler option
|
file | diff | annotate |
| Sun, 04 May 2014 18:14:59 +0200 |
added missing space between command-line options
|
file | diff | annotate |
| Fri, 04 Apr 2014 15:56:40 +0200 |
use Z3 TPTP cores rather than proofs since the latter are somewhat broken
|
file | diff | annotate |
| Fri, 04 Apr 2014 11:49:47 +0200 |
improved parsing of "z3_tptp" proofs
|
file | diff | annotate |
| Thu, 03 Apr 2014 17:16:02 +0200 |
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
|
file | diff | annotate |
| Thu, 03 Apr 2014 17:00:14 +0200 |
use Alt-Ergo 0.95.2, the latest and greatest version
|
file | diff | annotate |
| Thu, 03 Apr 2014 16:57:19 +0200 |
updated Z3 TPTP to 4.3.1+
|
file | diff | annotate |
| Wed, 18 Dec 2013 16:50:14 +0100 |
made SML/NJ happier
|
file | diff | annotate |
| Tue, 17 Dec 2013 14:03:29 +0100 |
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
|
file | diff | annotate |
| Thu, 24 Oct 2013 12:43:33 +0200 |
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
|
file | diff | annotate |
| Thu, 12 Sep 2013 22:10:57 +0200 |
prefixed types and some functions with "atp_" for disambiguation
|
file | diff | annotate |
| Wed, 11 Sep 2013 09:50:48 +0200 |
adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
|
file | diff | annotate |
| Wed, 28 Aug 2013 18:44:50 +0200 |
got rid of old error -- users who install SPASS manually are responsible for any version mismatches
|
file | diff | annotate |
| Tue, 13 Aug 2013 10:26:56 +0200 |
Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
|
file | diff | annotate |
| Mon, 29 Jul 2013 15:30:31 +0200 |
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
|
file | diff | annotate |
| Sun, 26 May 2013 14:02:03 +0200 |
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
|
file | diff | annotate |
| Tue, 21 May 2013 09:02:58 +0200 |
disabled choice in Satallax
|
file | diff | annotate |
| Tue, 21 May 2013 09:02:58 +0200 |
prefer compiled version of LEO-II and Satallax if available
|
file | diff | annotate |
| Tue, 21 May 2013 09:02:58 +0200 |
updated remote provers
|
file | diff | annotate |
| Mon, 20 May 2013 11:27:13 +0200 |
started adding agsyHOL as an experimental prover
|
file | diff | annotate |
| Wed, 15 May 2013 17:43:42 +0200 |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file | diff | annotate |
| Wed, 08 May 2013 15:47:19 +0200 |
use right default for "uncurried_aliases" with polymorphic SPASS
|
file | diff | annotate |
| Fri, 03 May 2013 10:27:24 +0200 |
tuning
|
file | diff | annotate |
| Fri, 03 May 2013 10:26:34 +0200 |
pass certain readability-enhancing Vampire options only when an Isar proof is needed
|
file | diff | annotate |
| Mon, 08 Apr 2013 12:11:06 +0200 |
robustness w.r.t. unknown arguments
|
file | diff | annotate |
| Wed, 20 Mar 2013 15:35:35 +0100 |
use the right role for SPASS hypotheses
|
file | diff | annotate |
| Tue, 05 Mar 2013 11:59:58 +0100 |
polymorphic SPASS is also SPASS
|
file | diff | annotate |
| Thu, 21 Feb 2013 12:22:26 +0100 |
swap slices so that the last slice is more complete (for minimization)
|
file | diff | annotate |
| Wed, 20 Feb 2013 15:26:19 +0100 |
upgraded to Alt-Ergo 0.95
|
file | diff | annotate |
| Wed, 20 Feb 2013 10:45:01 +0100 |
turn off more evil Vampire options to facilitate Isar proof generation
|
file | diff | annotate |
| Sun, 03 Feb 2013 17:31:33 +0100 |
tuned slicing (E-MaLeS and E-Par)
|
file | diff | annotate |
| Sat, 02 Feb 2013 17:25:55 +0100 |
tune slices further
|
file | diff | annotate |
| Sat, 02 Feb 2013 10:13:14 +0100 |
tweak ATP slices further
|
file | diff | annotate |
| Thu, 31 Jan 2013 17:54:05 +0100 |
tuned slices
|
file | diff | annotate |
| Thu, 31 Jan 2013 17:54:05 +0100 |
store fact filter along with ATP slice
|
file | diff | annotate |
| Thu, 17 Jan 2013 17:55:02 +0100 |
make SPASS more configurable, for experiments
|
file | diff | annotate |
| Thu, 17 Jan 2013 14:01:45 +0100 |
added E-Par support
|
file | diff | annotate |
| Mon, 03 Dec 2012 20:55:32 +0100 |
tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
|
file | diff | annotate |
| Wed, 31 Oct 2012 11:23:21 +0100 |
less verbose -- the warning will reach the users anyway by other means
|
file | diff | annotate |
| Wed, 31 Oct 2012 11:23:21 +0100 |
tuned messages
|
file | diff | annotate |
| Wed, 31 Oct 2012 11:23:21 +0100 |
added a timeout around script that relies on the network
|
file | diff | annotate |
| Wed, 31 Oct 2012 11:23:21 +0100 |
tuning
|
file | diff | annotate |
| Tue, 14 Aug 2012 16:09:45 +0200 |
tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
|
file | diff | annotate |
| Tue, 14 Aug 2012 15:23:28 +0200 |
tweak Vampire setup in the light of new evaluation
|
file | diff | annotate |
| Tue, 07 Aug 2012 22:54:27 +0200 |
proper quoting
|
file | diff | annotate |
| Tue, 07 Aug 2012 14:29:18 +0200 |
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
|
file | diff | annotate |
| Tue, 07 Aug 2012 13:03:50 +0200 |
specify full path to clausifier
|
file | diff | annotate |
| Mon, 06 Aug 2012 22:12:17 +0200 |
added iProver(-Eq) local
|
file | diff | annotate |
| Thu, 02 Aug 2012 10:10:29 +0200 |
support older versions of Vampire
|
file | diff | annotate |
| Thu, 02 Aug 2012 10:10:29 +0200 |
added E-MaLeS to list of provers for testing
|
file | diff | annotate |