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