Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

meson_dcutin : int ref

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,