#
8be3e9b7 |
|
25-Jan-2004 |
Joe Hurd <joe@gilith.com> |
Rationalized equality axioms for higher-order mode.
|
#
20ad9a14 |
|
28-Jul-2003 |
Joe Hurd <joe@gilith.com> |
Fixed a bug found by Michael Norrish whereby definitional CNF interacted badly with type reconstruction. This resulted in some invocations of METIS_TAC returning "error during proof translation", and then failing to find a proof with types switched on. All fixed now. Now that STRIP_TAC has changed, METIS_TAC can safely do pre-normalization splitting using DISJ_CASES_THEN. The only user-visible result of this should be better performance.
|
#
91bf4ed0 |
|
17-Jun-2003 |
Joe Hurd <joe@gilith.com> |
Version 1.3: 17 June 2002 Goals submitted to MESON_TAC when HOL is built .......... 1953 Proved by MESON_TAC ..................................... 1953 Proved by METIS_TAC within 10s .......................... 1946 Between Versions 1.2 and 1.3 * Implemention of definitional CNF to reduce blow-up in number of clauses (usually caused by nested boolean equivalences). * Resolution is more robust and efficient, and includes an option (off by default) for clauses to inherit ordering constraints.
|
#
c8d258c7 |
|
19-Nov-2002 |
Joe Hurd <joe@gilith.com> |
Version 1.2: 19 November 2002 Goals submitted to MESON_TAC when HOL is built .......... 1779 Proved by MESON_TAC ..................................... 1779 Proved by METIS_TAC within 10s .......................... 1774 Between Versions 1.1 and 1.2 * Ground-up reimplementation of the resolution calculus, which now performs ordered resolution and ordered paramodulation. * A single entry-point METIS_TAC, which uses heuristics to decide whether to apply FO_METIS_TAC or HO_METIS_TAC. * {HO|FO}_METIS_TAC both initially operate in typeless mode, and automatically try again with types if an error occurs during proof translation. * Extensionality axiom now included in HO_METIS_TAC by default.
|
#
01d2e53d |
|
18-Jul-2002 |
Joe Hurd <joe@gilith.com> |
Initial check-in of the Metis first-order prover.
|