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
|
\DOC meson_split_limit
\TYPE {meson_split_limit : int ref}
\SYNOPSIS
Limit initial case splits before {MESON} proper is applied.
\DESCRIBE
This is one of several parameters determining the behavior of {MESON},
{MESON_TAC} and related rules and tactics. Before these rules or tactics are
applied, the formula to be proved is often decomposed by splitting, for example
an equivalence {p <=> q} to two separate implications {p ==> q} and {q ==> p}.
This often makes the eventual proof much easier for {MESON}. On the other hand,
if splitting is applied too many times, it can become inefficient. The value
{meson_split_limit} (default {8}) is the maximum number of times that splitting
can be applied before {MESON} proper.
\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_depth, meson_prefine,
meson_skew.
\ENDDOC
|
