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
|
\DOC meson_depth
\TYPE {meson_depth : bool ref}
\SYNOPSIS
Make {MESON}'s search algorithm work by proof depth rather than size.
\DESCRIBE
This is one of several parameters determining the behavior of {MESON},
{MESON_TAC} and related rules and tactics. The basic search strategy is
iterated deepening, searching for proofs with higher and higher limits on the
search space. The flag {meson_depth}, when set to {true}, limits the search
space based on proof depth, i.e. the longest branch. When set to {false}, as it
is by default, the proof is limited based on total size.
\FAILURE
Not applicable.
\USES
For users requiring fine control over the algorithms used in {MESON}'s
first-order proof search.
\SEEALSO
meson_brand, meson_chatty, meson_dcutin, meson_prefine, meson_skew,
meson_split_limit,
\ENDDOC
|
