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
30
31
32
|
\DOC meson_skew
\TYPE {meson_skew : int ref}
\SYNOPSIS
Determines skew in {MESON} proof tree search limits.
\DESCRIBE
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
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.
\SEEALSO
meson_brand, meson_chatty, meson_dcutin, meson_depth, meson_prefine,
meson_split_limit,
\ENDDOC
|
