#
7ea28372 |
|
03-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make minor (semantically no-op) cleanups in src/metis
|
#
e4283b8e |
|
03-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use new Portable.make_counter in various places within src/metis
|
#
10308a8e |
|
31-Aug-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Isolate assignment to traces ref in metis code Hide assignment to this reference behind add_trace and set_traces function calls.
|
#
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.
|
#
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.
|
#
7850f004 |
|
21-Sep-2002 |
Joe Hurd <joe@gilith.com> |
Version 1.1 of the Metis Library. From the Change Log section of the README: Between Versions 1.0 and 1.1 * Added a "metis" entry to the HOL trace system: it nows prints status information during proof (if HOL is in interactive mode). * Restricted (universal and existential) quantifiers are now normalized by the NNF conversion. * (First-order) METIS_TAC can now handle boolean variables. * Improved performance in the model elimination proof procedure due to better caching (following a suggestion from John Harrison). * First-order substitutions are now fully Boultonized. * The first-order logical kernel makes local tweaks to keep proofs as small as possible.
|
#
01d2e53d |
|
18-Jul-2002 |
Joe Hurd <joe@gilith.com> |
Initial check-in of the Metis first-order prover.
|