Tue, 24 Jun 2014 12:36:45 +0200 |
blanchet |
added parentheses around type arguments in THF
|
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 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
|
Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
improved whitelist (cf. be1874de8344)
|
file |
diff |
annotate
|
Thu, 01 May 2014 09:30:35 +0200 |
haftmann |
optional case enforcement
|
file |
diff |
annotate
|
Fri, 25 Apr 2014 11:58:10 +0200 |
blanchet |
reintroduced '...' (nonexhaustive) syntax for SPASS-Pirate
|
file |
diff |
annotate
|
Thu, 19 Dec 2013 19:35:50 +0100 |
blanchet |
tuning 'case' expressions
|
file |
diff |
annotate
|
Thu, 19 Dec 2013 15:47:17 +0100 |
blanchet |
extended ATP types with sorts
|
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
|
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
|
Fri, 07 Jun 2013 22:17:22 -0400 |
blanchet |
SPASS has more Uppercase keywords than I was fearing -- better always append _
|
file |
diff |
annotate
|
Mon, 20 May 2013 12:35:29 +0200 |
blanchet |
freeze types in Sledgehammer goal, not just terms
|
file |
diff |
annotate
|
Mon, 20 May 2013 11:49:56 +0200 |
blanchet |
generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
|
file |
diff |
annotate
|
Mon, 20 May 2013 11:35:55 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
Thu, 16 May 2013 13:05:52 +0200 |
blanchet |
reintroduced syntax for "nonexhaustive" datatypes
|
file |
diff |
annotate
|
Thu, 16 May 2013 13:05:52 +0200 |
blanchet |
more work on SPASS datatypes
|
file |
diff |
annotate
|
Wed, 15 May 2013 18:39:20 +0200 |
blanchet |
more work on SPASS datatypes
|
file |
diff |
annotate
|
Wed, 15 May 2013 18:09:20 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Wed, 15 May 2013 18:06:40 +0200 |
blanchet |
no need to reinvent the wheel ("fold_map")
|
file |
diff |
annotate
|
Wed, 15 May 2013 18:05:46 +0200 |
blanchet |
more work on implementing datatype output for new SPASS
|
file |
diff |
annotate
|
Wed, 15 May 2013 17:49:39 +0200 |
blanchet |
tuned code
|
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, 15 May 2013 17:27:24 +0200 |
blanchet |
added datatype declaration syntax for next-gen SPASS
|
file |
diff |
annotate
|
Mon, 06 May 2013 11:03:08 +0200 |
smolkas |
handle dummy atp terms
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 15:19:14 +0200 |
blanchet |
work on CASC LTB ISA exporter
|
file |
diff |
annotate
|
Thu, 13 Dec 2012 23:22:10 +0100 |
blanchet |
generate original name as a comment in SPASS problems as well
|
file |
diff |
annotate
|
Thu, 13 Dec 2012 22:49:08 +0100 |
blanchet |
generate comments with original names for debugging
|
file |
diff |
annotate
|
Tue, 06 Nov 2012 11:20:56 +0100 |
blanchet |
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
|
file |
diff |
annotate
|
Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
renamed experimental option
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
finished implementation of DFG type class output
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
more work on DFG type classes
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
more work on class support
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
generate type classes for polymorphic DFG format (SPASS)
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
cleanly distinguish between type declarations and symbol declarations
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
added sorts to datastructure
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
implement polymorphic DFG output, without type classes for now
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
added type arguments to "ATerm" constructor -- but don't use them yet
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
started adding polymophic SPASS output
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
|
file |
diff |
annotate
|
Mon, 28 May 2012 20:25:38 +0200 |
blanchet |
don't generate definitions for LEO-II -- this cuases more harm than good
|
file |
diff |
annotate
|
Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
tuned names
|
file |
diff |
annotate
|
Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps"
|
file |
diff |
annotate
|
Wed, 25 Apr 2012 22:00:33 +0200 |
blanchet |
don't use the native choice operator if the type encoding isn't higher-order
|
file |
diff |
annotate
|
Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
tuning (in particular, Symtab instead of AList)
|
file |
diff |
annotate
|
Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
|
file |
diff |
annotate
|
Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
avoid DL
|
file |
diff |
annotate
|
Wed, 21 Mar 2012 16:53:24 +0100 |
blanchet |
generate weights and precedences for predicates as well
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 18:42:45 +0100 |
blanchet |
removed obsolete temporary hack
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 18:42:45 +0100 |
blanchet |
tweaks
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 10:45:52 +0100 |
blanchet |
don't generate new SPASS constructs for old SPASS
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
continued implementation of term ordering attributes
|
file |
diff |
annotate
|
Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
internal renamings
|
file |
diff |
annotate
|
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)
|
file |
diff |
annotate
|
Thu, 09 Feb 2012 14:42:18 +0100 |
blanchet |
minor DFG fix
|
file |
diff |
annotate
|
Thu, 09 Feb 2012 14:04:17 +0100 |
blanchet |
improved KBO weights -- beware of explicit applications
|
file |
diff |
annotate
|