| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 14:03:29 +0100 |
blanchet |
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
|
file |
diff |
annotate
|
| Thu, 24 Oct 2013 12:43:33 +0200 |
blanchet |
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 |
blanchet |
prefixed types and some functions with "atp_" for disambiguation
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 09:50:48 +0200 |
blanchet |
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 |
blanchet |
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 |
blanchet |
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 |
blanchet |
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 |
blanchet |
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 |
blanchet |
disabled choice in Satallax
|
file |
diff |
annotate
|
| Tue, 21 May 2013 09:02:58 +0200 |
blanchet |
prefer compiled version of LEO-II and Satallax if available
|
file |
diff |
annotate
|
| Tue, 21 May 2013 09:02:58 +0200 |
blanchet |
updated remote provers
|
file |
diff |
annotate
|
| Mon, 20 May 2013 11:27:13 +0200 |
blanchet |
started adding agsyHOL as an experimental prover
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Wed, 08 May 2013 15:47:19 +0200 |
blanchet |
use right default for "uncurried_aliases" with polymorphic SPASS
|
file |
diff |
annotate
|
| Fri, 03 May 2013 10:27:24 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 03 May 2013 10:26:34 +0200 |
blanchet |
pass certain readability-enhancing Vampire options only when an Isar proof is needed
|
file |
diff |
annotate
|
| Mon, 08 Apr 2013 12:11:06 +0200 |
blanchet |
robustness w.r.t. unknown arguments
|
file |
diff |
annotate
|
| Wed, 20 Mar 2013 15:35:35 +0100 |
blanchet |
use the right role for SPASS hypotheses
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 11:59:58 +0100 |
blanchet |
polymorphic SPASS is also SPASS
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 12:22:26 +0100 |
blanchet |
swap slices so that the last slice is more complete (for minimization)
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 15:26:19 +0100 |
blanchet |
upgraded to Alt-Ergo 0.95
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 10:45:01 +0100 |
blanchet |
turn off more evil Vampire options to facilitate Isar proof generation
|
file |
diff |
annotate
|
| Sun, 03 Feb 2013 17:31:33 +0100 |
blanchet |
tuned slicing (E-MaLeS and E-Par)
|
file |
diff |
annotate
|
| Sat, 02 Feb 2013 17:25:55 +0100 |
blanchet |
tune slices further
|
file |
diff |
annotate
|
| Sat, 02 Feb 2013 10:13:14 +0100 |
blanchet |
tweak ATP slices further
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
store fact filter along with ATP slice
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 17:55:02 +0100 |
blanchet |
make SPASS more configurable, for experiments
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 14:01:45 +0100 |
blanchet |
added E-Par support
|
file |
diff |
annotate
|