| #
20bbfd8d |
|
31-Aug-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Clean up some METIS library syntax (semantically a no-op)
Mostly deleting redundant infix declarations, but some other random
reformatting along the way
|
| #
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files.
This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!
|
| #
e6f1d9ff |
|
15-Jan-2005 |
Joe Hurd <joe@gilith.com> |
Improvements to Metis made while investigating bad performance reported
by Anthony, Juliano and Mike.
|
| #
8933c9c4 |
|
26-May-2004 |
Joe Hurd <joe@gilith.com> |
New version of metis: this one actually goes through the compiler
and runs the selftest!
|
| #
706836b9 |
|
14-Jan-2004 |
Joe Hurd <joe@gilith.com> |
Latest version of METIS_TAC.
The biggest change is that scheduling provers is done by number of
inferences, not time used, so METIS_TAC is now completely
deterministic. If it works for you on a subgoal, it will work every
time HOL4 is built.
|
| #
5d643e5d |
|
27-Jun-2003 |
Joe Hurd <joe@gilith.com> |
Fixed a bug discovered by Konrad, where the new version of metis couldn't
prove something the previous version could.
|
| #
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.
|