| 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
|
| Sun, 15 Dec 2013 19:01:06 +0100 |
blanchet |
use 'prop' rather than 'bool' systematically in Isar reconstruction code
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 18:54:26 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 22:20:01 +0100 |
blanchet |
whitespace tuning
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 19:42:30 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 19:36:24 +0100 |
blanchet |
more refactoring to accommodate SMT proofs
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:11:52 +0100 |
blanchet |
simplified old code
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 17:37:35 +0100 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 17:12:58 +0100 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 22:10:57 +0200 |
blanchet |
prefixed types and some functions with "atp_" for disambiguation
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 18:06:39 +0200 |
blanchet |
avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Thu, 16 May 2013 14:58:30 +0200 |
blanchet |
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
|
file |
diff |
annotate
|