forked from HOL-Theorem-Prover/HOL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathREADME
166 lines (115 loc) · 6.12 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
HOL4 Metis Library Documentation
Quick Guide to Using the HOL4 Metis Library
At the top of your proof script, write
load "metisLib";
open metisLib;
Opening the Metis library makes available the automatic provers
METIS_TAC : thm list -> tactic
METIS_PROVE : thm list -> term -> thm
which both take a list of theorems that are used to prove the subgoal.
Examples
prove (``?x. x``, METIS_TAC []);
prove (``!x. ~(x = 0) ==> ?!y. x = SUC y``,
METIS_TAC [numTheory.INV_SUC, arithmeticTheory.num_CASES]);
METIS_PROVE [prim_recTheory.LESS_SUC_REFL, arithmeticTheory.num_CASES]
``(!P. (!n. (!m. m < n ==> P m) ==> P n) ==> !n. P n) ==>
!P. P 0 /\ (!n. P n ==> P (SUC n)) ==> !n. P n``;
How It Works
This is how METIS_TAC proves a HOL subgoal:
1. First some HOL conversions and tactics simplify the subgoal and convert
it to conjunctive normal form.
2. The normalized problem is mapped to first-order syntax.
3. The Metis first-order prover attacks the first-order problem, hopefully
deriving a refutation.
4. The first-order refutation is translated to a HOL proof of the original
subgoal.
For more details on the interface please refer to the [1]System Description.
To find out more about the Metis first-order prover (including performance
information) you can visit its [2]own web page.
Comparison with MESON_TAC
METIS_TAC is generally slower than MESON_TAC on simple problems, but has
better coverage. For example, MESON_TAC cannot prove the following theorems:
METIS_PROVE [] ``?x. x``;
METIS_PROVE [] ``p (\x. x) /\ q ==> q /\ p (\y. y)``;
The combination of model elimination and resolution calculi in METIS_TAC
allows some hard theorems to be proved that are too deep for the HOL version
of MESON_TAC, such as the GILMORE_9 and STEAM_ROLLER problems. Also, the
ordered paramodulation used by the resolution component of METIS_TAC allows
it to prove harder equality problems. An example to illustrate this is the
following theorem:
METIS_PROVE []
``(!x y. x * y = y * x) /\ (!x y z. x * y * z = x * (y * z)) ==>
a * b * c * d * e * f = f * e * d * c * b * a``;
Known Bugs
At the present time all the bugs are unknown.
Credits
The HOL4 Metis library was written by Joe Hurd, based on John Harrison's
implementation of MESON_TAC. The library has been much improved by feedback
from HOL4 users, especially Michael Norrish, Konrad Slind and Mike Gordon.
Change Log
* 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.
* Changed the normalization to eliminate let terms.
Version 1.5: 14 January 2004
Subgoals proved by MESON_TAC when HOL is built .......... 2010
Proved by METIS_TAC within 10s .......................... 1998
Between Versions 1.4 and 1.5
* Scheduling provers is no longer based on time used, but rather number of
inferences.
* Simplification of resolution clauses using disequation literals.
* Implemented finite models to guide clause selection in resolution.
* The model elimination prover optimizes the order of rules and literals
within rules.
Version 1.4: 2 October 2003
Subgoals proved by MESON_TAC when HOL is built .......... 1982
Proved by METIS_TAC within 10s .......................... 1977
Between Versions 1.3 and 1.4
* Added an ordered resolution prover to the default set.
* Improved resolution performance with a special-purpose datatype for
inter-reducing equations.
Version 1.3: 18 June 2003
Subgoals proved by MESON_TAC when HOL is built .......... 1976
Proved by METIS_TAC within 10s .......................... 1971
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.
Version 1.2: 19 November 2002
Subgoals proved by MESON_TAC when HOL is built .......... 1779
Proved by METIS_TAC within 10s .......................... 1774
Between Versions 1.1 and 1.2
* Ground-up rewrite 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 theorem now included in HO_METIS_TAC by default.
Version 1.1: 21 September 2002
Subgoals proved by MESON_TAC when HOL is built .......... 1745
Proved by FO_METIS_TAC within 10s ....................... 1485
Proved by HO_METIS_TAC within 10s ....................... 1698
Proved by one of {FO|HO}_METIS_TAC within 10s ........... 1717
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.
* Improved performance in the model elimination proof procedure with
better caching (following a suggestion from John Harrison).
* First-order substitutions are now fully Boultonized.
* The first-order logical kernel automatically performs peep-hole
optimizations to keep proofs as small as possible.
Version 1.0: 18 July 2002
Subgoals proved by MESON_TAC when HOL is built .......... 1435
Proved by FO_METIS_TAC within 10s ....................... 1240
Proved by HO_METIS_TAC within 10s ....................... 1346
Proved by one of {FO|HO}_METIS_TAC within 10s ........... 1389
Metis the moon of Jupiter
References
1. http://www.cl.cam.ac.uk/~jeh1004/research/papers/hol2fol.html
2. http://www.cl.cam.ac.uk/~jeh1004/software/metis