| Wed, 18 Oct 2023 10:41:12 +0200 |
desharna |
added new portfolio for Vampire 4.8
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
more robust E proof parsing
|
file |
diff |
annotate
|
| Mon, 17 Oct 2022 13:04:00 +0200 |
blanchet |
generate some metainformation not only for SPASS but also for Zipperposition, for experimentation
|
file |
diff |
annotate
|
| Tue, 29 Mar 2022 12:50:30 +0200 |
blanchet |
nicer TPTP output
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
cleaned up obsolete E setup and a bit of SPASS
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 10:45:47 +0100 |
blanchet |
added parentheses in TPTP output -- seem necessary for some provers
|
file |
diff |
annotate
|
| Sun, 28 Nov 2021 21:16:35 +0100 |
desharna |
proper tptp_builtins
|
file |
diff |
annotate
|
| Sun, 21 Nov 2021 11:21:16 +0100 |
desharna |
proper proxy for Hilbert choice in TPTP output
|
file |
diff |
annotate
|
| Fri, 12 Nov 2021 00:10:16 +0100 |
desharna |
separated FOOL from $ite/$let in TPTP output
|
file |
diff |
annotate
|
| Thu, 11 Nov 2021 15:34:02 +0100 |
desharna |
tuned generation of TPTP with $ite/$let in higher-order logics
|
file |
diff |
annotate
|
| Tue, 19 Oct 2021 11:29:02 +0200 |
desharna |
refactored tptp_builtins in Sledgehammer
|
file |
diff |
annotate
|
| Fri, 20 Aug 2021 17:57:57 +0200 |
desharna |
fixed $ite syntax in TPTP TFX generation
|
file |
diff |
annotate
|
| Mon, 16 Aug 2021 13:00:55 +0200 |
desharna |
fixed $ite syntax in TPTP THX generation
|
file |
diff |
annotate
|
| Tue, 27 Jul 2021 10:36:22 +0200 |
desharna |
added support for TFX $let to Sledgehammer's TPTP output
|
file |
diff |
annotate
|
| Thu, 17 Jun 2021 12:57:22 +0200 |
desharna |
added support for TFX's and THF's $ite to Sledgehammer
|
file |
diff |
annotate
|
| Thu, 03 Dec 2020 17:40:31 +0100 |
desharna |
proper proxification for fool + refactoring
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 18:45:19 +0100 |
desharna |
proper parsing of type encoding;
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 18:06:36 +0100 |
desharna |
proper handling of builtins in TFX
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 13:47:29 +0100 |
desharna |
proper generation of TPTP output for higher order builtins
|
file |
diff |
annotate
|
| Thu, 19 Nov 2020 15:11:37 +0100 |
desharna |
reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585
|
file |
diff |
annotate
|
| Thu, 19 Nov 2020 14:43:50 +0100 |
desharna |
renamed data type
|
file |
diff |
annotate
|
| Wed, 18 Nov 2020 13:44:34 +0100 |
desharna |
Tuned parentheses in TPTP output
|
file |
diff |
annotate
|
| Thu, 05 Nov 2020 18:14:02 +0100 |
desharna |
Added support for TFX to Sledgehammer
|
file |
diff |
annotate
|
| Fri, 02 Oct 2020 10:18:50 +0200 |
desharna |
Add more tacing to sledgehammer_isar_trace
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 17:22:09 +0100 |
blanchet |
tune ATP settings
|
file |
diff |
annotate
|
| Tue, 22 May 2018 17:15:02 +0200 |
blanchet |
added lambda-free HO output for Ehoh (higher-order E prototype)
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 13:48:17 +0100 |
wenzelm |
uniform use of Standard ML op-infix -- eliminated warnings;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 20:02:51 +0100 |
blanchet |
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 21:49:49 +0100 |
blanchet |
make sure that function types are never generated as '> @ A @ B', but always as 'A > B'
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
get rid of 'individual' type in DFG proofs
|
file |
diff |
annotate
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
put comments between TPTP lines to comply with TPTP BNF
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch hilbert_choice_support
|
file |
diff |
annotate
|
| 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
|