| Thu, 16 Aug 2012 15:41:36 +0200 |
blanchet |
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
renamed experimental option
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
add missing timeout multiplier
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
renamed TPTP commands to agree with Sutcliffe's terminology
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
don't use aggressive with HO ATP
|
file |
diff |
annotate
|
| Thu, 24 May 2012 18:21:54 +0200 |
blanchet |
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)
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 21 May 2012 10:39:32 +0200 |
blanchet |
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
|
file |
diff |
annotate
|
| Mon, 30 Apr 2012 21:59:10 +0200 |
blanchet |
export more symbols
|
file |
diff |
annotate
|
| Sun, 29 Apr 2012 11:44:33 +0200 |
blanchet |
split into demo and competitive version
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:36:27 +0200 |
blanchet |
use Nitpick as an oracle for finite problems
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:36:27 +0200 |
blanchet |
add extensionality to first-order provers
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 15:24:37 +0200 |
blanchet |
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 15:24:37 +0200 |
blanchet |
move LEO-II closer to the top, for testing
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 15:24:37 +0200 |
blanchet |
smaller batches, to play safe
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 13:19:21 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 12:16:10 +0200 |
blanchet |
more tweaking of TPTP/CASC setup
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 01:05:06 +0200 |
blanchet |
further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 00:28:06 +0200 |
blanchet |
tuning; no need for relevance filter
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 22:00:33 +0200 |
blanchet |
more work on TPTP Isabelle and Sledgehammer tactics
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 22:00:33 +0200 |
blanchet |
more work on CASC setup
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 14:33:21 +0200 |
blanchet |
tweak TPTP Nitpick's output
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
get rid of old parser, hopefully for good
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:46 +0200 |
blanchet |
added timeout argument to TPTP tools
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 11:15:49 +0200 |
blanchet |
prepend PWD to relative paths
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 11:15:49 +0200 |
blanchet |
reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 23:13:11 +0200 |
blanchet |
remove old TPTP CNF/FOF parser; always use Nik's new parser
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 22:40:25 +0200 |
blanchet |
tuned SZS status output
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 22:16:05 +0200 |
blanchet |
started integrating Nik's parser into TPTP command-line tools
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
implemented "tptp_refute" tool
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
added problem importer
|
file |
diff |
annotate
|