History log of /seL4-l4v-10.1.1/HOL4/src/metis/mlibClauseset.sml
Revision Date Author Comments
# 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.


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


# 82c76808 21-Jan-2004 Joe Hurd <joe@gilith.com>

* Implemented a HOL specific finite model, which knows about
numbers, lists and sets.
* Removed multiple provers: METIS_TAC is now solely based on ordered
resolution.


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


# 50c3995d 02-Oct-2003 Joe Hurd <joe@gilith.com>

New version of metis with a more powerful prover engine.


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


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