- SYNOPSIS
-
Determines cut-in point for divide-and-conquer refinement in MESON.
- DESCRIPTION
-
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 CONDITIONS
-
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.
- SEE ALSO
-
meson_brand, meson_chatty, meson_depth, meson_prefine, meson_skew,
meson_split_limit,