| 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
|