| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
SPASS-Pirate is now called Pirate
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sun, 12 Oct 2014 21:52:45 +0200 |
blanchet |
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
|
file |
diff |
annotate
|
| Sun, 12 Oct 2014 21:52:44 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
avoid creating needless skolemization steps for SPASS
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
get rid of 'individual' type in DFG proofs
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
slightly nicer names
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
improved unskolemization of SPASS problems
|
file |
diff |
annotate
|
| Tue, 30 Sep 2014 16:01:46 +0200 |
blanchet |
proper types for applied variables, for typed formats (TFF0, DFG)
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 20:26:04 +0200 |
blanchet |
support hypotheses with schematics in Isar proofs
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
parse back type of SPASS proof variables
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 23:48:46 +0200 |
blanchet |
reworked unskolemization for SPASS
|
file |
diff |
annotate
|
| Sat, 09 Aug 2014 21:03:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 10:59:40 +0200 |
blanchet |
rationalize Skolem names
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 10:02:35 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 09:58:23 +0200 |
blanchet |
don't rename variables which will be renamed later anyway
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 09:55:42 +0200 |
blanchet |
normalize skolem argument variable names so that they coincide when taking the conjunction
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 09:20:00 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 16:53:09 +0200 |
blanchet |
deal with E definitions
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 23:29:50 +0200 |
blanchet |
fine-tuned Isar reconstruction, esp. boolean simplifications
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 23:29:49 +0200 |
blanchet |
centralized boolean simplification so that e.g. LEO-II benefits from it
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 20:44:29 +0200 |
blanchet |
better handling of variable names
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Whitespace and indentation correction.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch hilbert_choice_support
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch satallax_proof_support_Sledgehammer
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:11 +0200 |
fleury |
removing the '= True' generated by Leo-II.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 00:50:41 +0200 |
blanchet |
also try 'metis' with 'full_types'
|
file |
diff |
annotate
|
| Mon, 28 Jul 2014 10:57:33 +0200 |
blanchet |
correctly translate THF functions from terms to types
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
more robust handling of types for skolems (modeled as Frees)
|
file |
diff |
annotate
|
| Sat, 12 Jul 2014 11:31:23 +0200 |
blanchet |
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:42:44 +0200 |
blanchet |
integrated new Waldmeister code with 'sledgehammer' command
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:40:59 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:21:52 +0200 |
fleury |
Moving the remote prefix deleting on Sledgehammer's side
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:21:39 +0200 |
fleury |
Correcting the type parser
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:18:34 +0200 |
fleury |
imported patch leo2_skolem_simplication
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:18:15 +0200 |
fleury |
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 11:38:53 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 04 May 2014 19:27:28 +0200 |
blanchet |
fixed Waldmeister endgame w.r.t. "Trueprop"
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 14:48:20 +0100 |
blanchet |
correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:19:07 +0100 |
blanchet |
merged 'reconstructors' and 'proof methods'
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
rationalized threading of 'metis' arguments
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 22:42:29 +0100 |
blanchet |
reverted unsound optimization
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 20:39:49 +0100 |
blanchet |
unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:40:31 +0100 |
blanchet |
centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn)
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 17:11:54 +0100 |
blanchet |
pick up tfree/tvar type from SPASS-Pirate proof
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 16:11:20 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 15:47:17 +0100 |
blanchet |
extended ATP types with sorts
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 15:04:21 +0100 |
blanchet |
removed debugging output
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 14:57:21 +0100 |
blanchet |
honor SPASS-Pirate type arguments
|
file |
diff |
annotate
|
| Wed, 18 Dec 2013 22:55:20 +0100 |
blanchet |
parse SPASS-Pirate types
|
file |
diff |
annotate
|
| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 14:15:23 +0100 |
blanchet |
tuning
|
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
|
| Tue, 17 Dec 2013 09:42:38 +0100 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 23:05:16 +0100 |
blanchet |
handle Skolems gracefully for SPASS as well
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 20:24:13 +0100 |
blanchet |
reverse Skolem function arguments
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:18:52 +0100 |
blanchet |
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
|
file |
diff |
annotate
|