| Tue, 01 Aug 2006 13:44:05 +0200 |
mengj |
Added in code to check too general axiom clauses.
|
file |
diff |
annotate
|
| Sat, 15 Jul 2006 13:50:26 +0200 |
mengj |
Only include combinators if required by goals and user specified lemmas.
|
file |
diff |
annotate
|
| Thu, 13 Jul 2006 17:39:56 +0200 |
paulson |
"conjecture" must be lower case
|
file |
diff |
annotate
|
| Thu, 06 Jul 2006 12:18:17 +0200 |
paulson |
some tidying; fixed the output of theorem names
|
file |
diff |
annotate
|
| Wed, 05 Jul 2006 14:22:09 +0200 |
mengj |
Literals aren't sorted any more.
|
file |
diff |
annotate
|
| Thu, 29 Jun 2006 18:11:15 +0200 |
paulson |
added the "th" field to datatype Clause
|
file |
diff |
annotate
|
| Mon, 29 May 2006 17:38:02 +0200 |
paulson |
warnings to debug outputs; default translation to const-typed
|
file |
diff |
annotate
|
| Thu, 25 May 2006 14:08:55 +0200 |
mengj |
Changed the DFG format's functions' declaration procedure.
|
file |
diff |
annotate
|
| Thu, 25 May 2006 11:53:01 +0200 |
mengj |
Fixed a bug.
|
file |
diff |
annotate
|
| Thu, 25 May 2006 08:09:10 +0200 |
mengj |
HOL problems now have DFG output format.
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 05:59:32 +0200 |
mengj |
changed the functions for getting HOL helper clauses.
|
file |
diff |
annotate
|
| Sat, 22 Apr 2006 06:06:39 +0200 |
mengj |
Changed the treatment of equalities.
|
file |
diff |
annotate
|
| Tue, 18 Apr 2006 05:38:18 +0200 |
mengj |
Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
|
file |
diff |
annotate
|
| Fri, 07 Apr 2006 05:12:51 +0200 |
mengj |
tptp_write_file accepts axioms as thm.
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 03:59:48 +0100 |
mengj |
Added tptp_write_file to write all necessary ATP input clauses to one file.
|
file |
diff |
annotate
|
| Thu, 23 Feb 2006 13:00:18 +0100 |
mengj |
Default type level is T_FULL now.
|
file |
diff |
annotate
|
| Mon, 30 Jan 2006 15:31:31 +0100 |
paulson |
tidy-up of res_clause.ML, removing the "predicates" field
|
file |
diff |
annotate
|
| Fri, 20 Jan 2006 04:35:23 +0100 |
mengj |
fixed a bug
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:06:08 +0100 |
paulson |
new hash table module in HOL/Too/s
|
file |
diff |
annotate
|
| Tue, 20 Dec 2005 04:29:25 +0100 |
mengj |
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
|
file |
diff |
annotate
|
| Tue, 06 Dec 2005 06:21:07 +0100 |
mengj |
Added new type embedding methods for translating HOL clauses.
|
file |
diff |
annotate
|
| Mon, 28 Nov 2005 07:17:07 +0100 |
mengj |
Added flags for setting and detecting whether a problem needs combinators.
|
file |
diff |
annotate
|
| Fri, 18 Nov 2005 07:10:00 +0100 |
mengj |
-- terms are fully typed.
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 02:23:49 +0200 |
mengj |
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
|
file |
diff |
annotate
|