Mon, 28 Nov 2005 07:16:16 +0100 Only output types if !keep_types is true.
mengj [Mon, 28 Nov 2005 07:16:16 +0100] rev 18275
Only output types if !keep_types is true.
Mon, 28 Nov 2005 07:15:38 +0100 Added two functions for CNF translation, used by other files.
mengj [Mon, 28 Nov 2005 07:15:38 +0100] rev 18274
Added two functions for CNF translation, used by other files.
Mon, 28 Nov 2005 07:15:13 +0100 Added in four control flags for HOL and FOL translations.
mengj [Mon, 28 Nov 2005 07:15:13 +0100] rev 18273
Added in four control flags for HOL and FOL translations. Changed functions that perform HOL/FOL translations, and write ATP input to files. Removed some functions that are no longer needed.
Mon, 28 Nov 2005 07:14:12 +0100 Slight modification to trace information.
mengj [Mon, 28 Nov 2005 07:14:12 +0100] rev 18272
Slight modification to trace information.
Mon, 28 Nov 2005 07:13:43 +0100 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
mengj [Mon, 28 Nov 2005 07:13:43 +0100] rev 18271
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.
Mon, 28 Nov 2005 07:12:01 +0100 Only output arities and class relations if !ResClause.keep_types is true.
mengj [Mon, 28 Nov 2005 07:12:01 +0100] rev 18270
Only output arities and class relations if !ResClause.keep_types is true.
Mon, 28 Nov 2005 05:03:00 +0100 some small tuning
urbanc [Mon, 28 Nov 2005 05:03:00 +0100] rev 18269
some small tuning
Mon, 28 Nov 2005 00:25:43 +0100 ISAR-fied two proofs about equality for abstraction functions.
urbanc [Mon, 28 Nov 2005 00:25:43 +0100] rev 18268
ISAR-fied two proofs about equality for abstraction functions.
Sun, 27 Nov 2005 20:06:24 +0100 * Provers/induct: obtain pattern;
wenzelm [Sun, 27 Nov 2005 20:06:24 +0100] rev 18267
* Provers/induct: obtain pattern;
Sun, 27 Nov 2005 06:01:11 +0100 added an authors section (please let me know if somebody is left out or unhappy)
urbanc [Sun, 27 Nov 2005 06:01:11 +0100] rev 18266
added an authors section (please let me know if somebody is left out or unhappy)
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip