#
fe9da3ea |
|
15-Dec-2016 |
blanchet <none@none> |
updated CASC instructions + tuning
|
#
0ef899fa |
|
15-Nov-2016 |
blanchet <none@none> |
generalized experimental feature slightly
|
#
6ef84525 |
|
27-Mar-2016 |
blanchet <none@none> |
refined experimental option of Sledgehammer
|
#
c8a3ab07 |
|
05-Mar-2016 |
wenzelm <none@none> |
tuned signature -- clarified modules; --HG-- rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML
|
#
4297b1e3 |
|
19-Dec-2015 |
blanchet <none@none> |
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
|
#
ee55c33d |
|
04-Nov-2015 |
blanchet <none@none> |
eliminated Nitpick's pedantic support for 'emdash'
|
#
75101fc4 |
|
02-Oct-2015 |
blanchet <none@none> |
better compliance with TPTP SZS standard
|
#
a982c8ed |
|
22-Jun-2015 |
blanchet <none@none> |
use CVC4 instead of CVC3 at CASC
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
76c7446c |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued obsolete Output.urgent_message;
|
#
ec76ee03 |
|
06-Aug-2014 |
blanchet <none@none> |
make TPTP tools work on polymorphic (TFF1) problems as well
|
#
563ba682 |
|
06-Aug-2014 |
blanchet <none@none> |
treat variables as frees in 'conjecture's
|
#
8c20ae01 |
|
12-Jul-2014 |
blanchet <none@none> |
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
|
#
97012828 |
|
16-Jun-2014 |
blanchet <none@none> |
compile
|
#
c5b00bcc |
|
02-Jun-2014 |
fleury <none@none> |
basic setup for zipperposition prover
|
#
fed5d9bd |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
#
a16c4f61 |
|
31-Jan-2014 |
blanchet <none@none> |
compile
|
#
b58b6956 |
|
31-Jan-2014 |
blanchet <none@none> |
renamed ML file --HG-- rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
|
#
67f491eb |
|
31-Jan-2014 |
blanchet <none@none> |
tuned ML file name --HG-- rename : src/HOL/Tools/Nitpick/nitpick_isar.ML => src/HOL/Tools/Nitpick/nitpick_commands.ML
|
#
c83d0af5 |
|
21-Nov-2013 |
blanchet <none@none> |
renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
|
#
40798651 |
|
18-Nov-2013 |
blanchet <none@none> |
send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
|
#
35143236 |
|
14-Nov-2013 |
blanchet <none@none> |
implemented 'tptp_translate'
|
#
42e9b2b9 |
|
30-Jul-2013 |
wenzelm <none@none> |
type theory is purely value-oriented;
|
#
1d90a75e |
|
19-May-2013 |
blanchet <none@none> |
made "completish" mode a bit more complete
|
#
e232176f |
|
16-May-2013 |
blanchet <none@none> |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
4ce7b0a2 |
|
27-Mar-2013 |
wenzelm <none@none> |
clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
|
#
36418877 |
|
31-Oct-2012 |
blanchet <none@none> |
moved Refute to "HOL/Library" to speed up building "Main" even more --HG-- rename : src/HOL/Refute.thy => src/HOL/Library/Refute.thy rename : src/HOL/Tools/refute.ML => src/HOL/Library/refute.ML
|
#
c13f9e2e |
|
31-Oct-2012 |
blanchet <none@none> |
use metaquantification when possible in Isar proofs
|
#
a2d2e5bf |
|
16-Aug-2012 |
blanchet <none@none> |
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
|
#
635a0ac2 |
|
26-Jun-2012 |
blanchet <none@none> |
renamed experimental option
|
#
b5ae9236 |
|
06-Jun-2012 |
blanchet <none@none> |
add missing timeout multiplier
|
#
f911a212 |
|
06-Jun-2012 |
blanchet <none@none> |
renamed TPTP commands to agree with Sutcliffe's terminology --HG-- rename : src/HOL/TPTP/lib/Tools/tptp_isabelle_comp => src/HOL/TPTP/lib/Tools/tptp_isabelle rename : src/HOL/TPTP/lib/Tools/tptp_isabelle_demo => src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
|
#
fc42e859 |
|
06-Jun-2012 |
blanchet <none@none> |
don't use aggressive with HO ATP
|
#
0c89260f |
|
24-May-2012 |
blanchet <none@none> |
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
|
#
0bfd4fed |
|
22-May-2012 |
blanchet <none@none> |
compile
|
#
0c3297b3 |
|
21-May-2012 |
blanchet <none@none> |
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
|
#
21ccf21a |
|
30-Apr-2012 |
blanchet <none@none> |
export more symbols
|
#
8a985e8c |
|
29-Apr-2012 |
blanchet <none@none> |
split into demo and competitive version --HG-- rename : src/HOL/TPTP/lib/Tools/tptp_isabelle => src/HOL/TPTP/lib/Tools/tptp_isabelle_demo
|
#
4f850aca |
|
27-Apr-2012 |
blanchet <none@none> |
use Nitpick as an oracle for finite problems
|
#
0e921175 |
|
27-Apr-2012 |
blanchet <none@none> |
add extensionality to first-order provers
|
#
6ce0bd41 |
|
27-Apr-2012 |
blanchet <none@none> |
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
|
#
1b2741c5 |
|
27-Apr-2012 |
blanchet <none@none> |
move LEO-II closer to the top, for testing
|
#
bb3eb48a |
|
27-Apr-2012 |
blanchet <none@none> |
smaller batches, to play safe
|
#
2d907cd2 |
|
27-Apr-2012 |
blanchet <none@none> |
tuning
|
#
90997541 |
|
26-Apr-2012 |
blanchet <none@none> |
more tweaking of TPTP/CASC setup
|
#
45893422 |
|
25-Apr-2012 |
blanchet <none@none> |
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
|
#
845a9656 |
|
25-Apr-2012 |
blanchet <none@none> |
tuning; no need for relevance filter
|
#
eb9a750b |
|
25-Apr-2012 |
blanchet <none@none> |
more work on TPTP Isabelle and Sledgehammer tactics
|
#
d99f3ac7 |
|
25-Apr-2012 |
blanchet <none@none> |
more work on CASC setup
|
#
316fb4bf |
|
25-Apr-2012 |
blanchet <none@none> |
tweak TPTP Nitpick's output
|
#
f3b947b9 |
|
24-Apr-2012 |
blanchet <none@none> |
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
|
#
f40e9657 |
|
24-Apr-2012 |
blanchet <none@none> |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
#
2c8eb630 |
|
24-Apr-2012 |
blanchet <none@none> |
get rid of old parser, hopefully for good
|
#
8dc6a48b |
|
22-Apr-2012 |
blanchet <none@none> |
added timeout argument to TPTP tools
|
#
3490aa61 |
|
21-Apr-2012 |
blanchet <none@none> |
prepend PWD to relative paths
|
#
5b3318fd |
|
21-Apr-2012 |
blanchet <none@none> |
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
|
#
7324d12f |
|
18-Apr-2012 |
blanchet <none@none> |
remove old TPTP CNF/FOF parser; always use Nik's new parser
|
#
00e83fcc |
|
18-Apr-2012 |
blanchet <none@none> |
tuned SZS status output
|
#
16412bdd |
|
18-Apr-2012 |
blanchet <none@none> |
started integrating Nik's parser into TPTP command-line tools
|
#
5e652fe1 |
|
23-Jan-2012 |
blanchet <none@none> |
implemented "tptp_refute" tool
|
#
cadbf5cb |
|
23-Jan-2012 |
blanchet <none@none> |
added problem importer
|