1\DOC GEN_MESON_TAC
2
3\TYPE {GEN_MESON_TAC : int -> int -> int -> thm list -> tactic}
4
5\SYNOPSIS
6Performs first order proof search to prove the goal, using both the
7given theorems and the assumptions in the search.
8
9\KEYWORDS
10decision procedure, tactic.
11
12\LIBRARY
13mesonLib
14
15\DESCRIBE
16{GEN_MESON_TAC} is the function which provides the underlying
17implementation of the model elimination solver used by both
18{MESON_TAC} and {ASM_MESON_TAC}.  The three integer parameters
19correspond to various ways in which the search can be tuned.
20
21The first is the minimum depth at which to search.  Setting this to a
22number greater than zero can save time if its clear that there will
23not be a proof of such a small depth.  {ASM_MESON_TAC} and {MESON_TAC}
24always use a value of 0 for this parameter.
25
26The second is the maximum depth to which to search.  Setting this low
27will stop the search taking too long, but may cause the engine to miss
28proofs it would otherwise find.  The setting of this variable for
29{ASM_MESON_TAC} and {MESON_TAC} is done through the reference variable
30{mesonLib.max_depth}.  This is set to 30 by default, but most proofs
31do not need anything like this depth.
32
33The third parameter is the increment used to increase the depth of
34search done by the proof search procedure.
35
36The approach used is iterative deepening, so with a call to
37{
38  GEN_MESON_TAC mn mx inc
39}
40the algorithm looks for a proof of depth {mn}, then for one
41of depth {mn + inc}, then at depth {mn + 2 * inc} etc.  Once the depth
42gets greater than {mx}, the proof search stops.
43
44\FAILURE
45{GEN_MESON_TAC} fails if it searches to a depth equal to the second
46integer parameter without finding a proof.  Shouldn't fail otherwise.
47
48
49
50\USES
51The construction of tailored versions of {MESON_TAC} and {ASM_MESON_TAC}.
52
53\SEEALSO
54mesonLib.ASM_MESON_TAC, mesonLib.MESON_TAC.
55\ENDDOC
56