| Wed, 03 Jan 2007 10:59:06 +0100 |
paulson |
first version of structured proof reconstruction
|
file |
diff |
annotate
|
| Fri, 22 Dec 2006 21:00:42 +0100 |
paulson |
tidying the ATP communications
|
file |
diff |
annotate
|
| Wed, 20 Dec 2006 17:03:46 +0100 |
paulson |
change from "Array" to "Vector"
|
file |
diff |
annotate
|
| Fri, 06 Oct 2006 15:39:29 +0200 |
paulson |
Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 16:01:48 +0200 |
paulson |
clearout of obsolete code
|
file |
diff |
annotate
|
| Fri, 25 Aug 2006 18:46:24 +0200 |
paulson |
using inc
|
file |
diff |
annotate
|
| Wed, 19 Apr 2006 10:43:53 +0200 |
paulson |
fix to spacing in switches, for Vampire under SML/NJ
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 17:57:09 +0100 |
paulson |
exporting reapAll and killChild
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 04:01:25 +0100 |
mengj |
Proof reconstruction now only takes names of theorems as input.
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 18:28:55 +0100 |
paulson |
better reporting
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:13 +0100 |
wenzelm |
Output.debug;
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 15:08:28 +0200 |
paulson |
code restructuring
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 11:29:24 +0200 |
paulson |
more tidying. Fixed process management bugs and race condition
|
file |
diff |
annotate
|
| Thu, 06 Oct 2005 10:14:22 +0200 |
paulson |
major simplification: removal of the goalstring argument
|
file |
diff |
annotate
|
| Wed, 05 Oct 2005 11:18:06 +0200 |
paulson |
improved process handling. tidied
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 09:59:01 +0200 |
paulson |
fixed the ascii-armouring of goalstring
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 12:44:25 +0200 |
paulson |
moved concat_with_and to watcher.ML
|
file |
diff |
annotate
|
| Wed, 28 Sep 2005 11:16:27 +0200 |
paulson |
time limit option; fixed bug concerning first line of ATP output
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 14:09:48 +0200 |
paulson |
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 18:35:19 +0200 |
paulson |
trying to limit the looping
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 18:43:39 +0200 |
paulson |
tidying, and support for axclass/classrel clauses
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 13:17:55 +0200 |
paulson |
further tidying; killing of old Watcher loops
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 18:30:22 +0200 |
paulson |
further simplification of the Isabelle-ATP linkup
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 15:12:13 +0200 |
paulson |
simplification of the Isabelle-ATP code; hooks for batch generation of problems
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 11:39:09 +0200 |
paulson |
PARTIAL conversion to Vampire8
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:46:00 +0200 |
paulson |
massive tidy-up and simplification
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 17:47:37 +0200 |
paulson |
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
|
file |
diff |
annotate
|
| Thu, 08 Sep 2005 17:35:02 +0200 |
paulson |
consolidation of duplicate code in Isabelle-ATP linkup
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 18:14:26 +0200 |
paulson |
Progress on eprover linkup, also massive tidying
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 09:54:31 +0200 |
paulson |
axioms now included in tptp files, no /bin/cat and various tidying
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 21:29:33 +0200 |
quigley |
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 17:55:24 +0200 |
paulson |
further tidying up of Isabelle-ATP link
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 15:25:44 +0200 |
paulson |
tidying up the Isabelle/ATP interface
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 11:45:54 +0200 |
paulson |
improved formatting
|
file |
diff |
annotate
|
| Fri, 26 Aug 2005 19:36:07 +0200 |
quigley |
DFG output now works for untyped rules (ML "ResClause.untyped();")
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 13:09:21 +0200 |
paulson |
no need for TPTP2X unless SPASS is used
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:26 +0200 |
wenzelm |
open ReconPrelim Recon_Transfer;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2005 16:42:42 +0200 |
quigley |
Fixed some problems with the signal handler.
|
file |
diff |
annotate
|
| Mon, 04 Jul 2005 15:51:56 +0200 |
quigley |
Streamlined the signal handler in watcher.ML
|
file |
diff |
annotate
|
| Fri, 24 Jun 2005 16:18:41 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Wed, 22 Jun 2005 20:26:31 +0200 |
quigley |
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 23:44:18 +0200 |
quigley |
Integrated vampire lemma code.
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 13:34:24 +0200 |
paulson |
VAMPIRE_HOME, helper_path and various stylistic tweaks
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 18:39:24 +0200 |
quigley |
Added VampCommunication.ML.
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 15:55:44 +0200 |
paulson |
using TPTP2X_HOME; indentation, etc
|
file |
diff |
annotate
|
| Fri, 10 Jun 2005 16:15:36 +0200 |
quigley |
All subgoals sent to the watcher at once now.
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 11:31:23 +0200 |
wenzelm |
File.platform_path vs. File.shell_path;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 15:54:11 +0200 |
quigley |
Added time lime (60 secs) to Spass calls.
|
file |
diff |
annotate
|
| Tue, 31 May 2005 12:42:36 +0200 |
quigley |
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
|
file |
diff |
annotate
|
| Fri, 27 May 2005 12:12:05 +0200 |
paulson |
Now uses File.write and File.append
|
file |
diff |
annotate
|
| Thu, 26 May 2005 18:34:23 +0200 |
paulson |
further tweaks to the SPASS setup
|
file |
diff |
annotate
|
| Thu, 26 May 2005 16:50:07 +0200 |
paulson |
trying to set up portable calling sequences for SPASS and tptp2X
|
file |
diff |
annotate
|
| Tue, 24 May 2005 10:23:24 +0200 |
paulson |
A new structure and reduced indentation
|
file |
diff |
annotate
|
| Mon, 23 May 2005 00:18:51 +0200 |
quigley |
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
|
file |
diff |
annotate
|
| Tue, 03 May 2005 14:27:21 +0200 |
quigley |
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 15:05:24 +0200 |
paulson |
added hearder lines and deleted some redundant material
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 10:05:06 +0200 |
paulson |
improved SML/NJ compatibility, etc.
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 18:01:50 +0200 |
quigley |
Corrected the problem with the ATP directory.
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 18:08:44 +0200 |
paulson |
more tidying of libraries in Reconstruction
|
file |
diff |
annotate
|