- SYNOPSIS
-
Determines skew in MESON proof tree search limits.
- DESCRIPTION
-
This is one of several parameters determining the behavior of MESON,
MESON_TAC and related rules and tactics. During search, MESON successively
searches for proofs of larger and larger `size'. The ``skew'' value determines
what proportion of the entire proof size is permitted in the left-hand half of
the list of subgoals. The symmetrical value is 2 (meaning one half), the
default setting of 3 (one third) seems generally better because it can cut
down on redundancy in proofs.
- 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 MESON's search strategy, see Harrison's paper
``Optimizing Proof Search in Model Elimination'', CADE-13, 1996.
- SEE ALSO
-
meson_brand, meson_chatty, meson_dcutin, meson_depth, meson_prefine,
meson_split_limit,