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
|
\DOC meson_dcutin
\TYPE {meson_dcutin : int ref}
\SYNOPSIS
Determines cut-in point for divide-and-conquer refinement in {MESON}.
\DESCRIBE
This is one of several parameters determining the behavior of {MESON},
{MESON_TAC} and related rules and tactics. This number (by default 1)
determines the number of current subgoals at which point a special
divide-and-conquer refinement will be invoked.
\FAILURE
Not applicable.
\USES
For users requiring fine control over the algorithms used in {MESON}'s
first-order proof search.
\COMMENTS
For more details of this optimization, see Harrison's paper ``Optimizing
Proof Search in Model Elimination'', CADE-13, 1996.
\SEEALSO
meson_brand, meson_chatty, meson_depth, meson_prefine, meson_skew,
meson_split_limit,
\ENDDOC
|
