#
499ad7b5 |
|
03-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Label assignments (v := e) as (* OK *) in src/metis These labels are my judgement that the references are strictly local and so not a concurrency issue. Additionally, some assignments in comments (to Moscow ML specific quietdec, for example) have just been deleted.
|
#
ea7bf382 |
|
01-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement more of Basis2002 for Moscow ML (adding Vector, Array, ArraySlice and VectorSlice), simplifying what Poly/ML has to emulate. Haven't done full rebuild test, but have got as far as integerTheory and Omega, which makes heavy uses of Vector etc.
|
#
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.
|
#
e475071e |
|
20-Oct-2003 |
Joe Hurd <joe@gilith.com> |
New version of Metis: + Uses finite models to guide clause selection in resolution. + A Metis test for when HOL is compiled using MLton.
|
#
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.
|