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
|
\DOC meson_prefine
\TYPE {meson_prefine : bool ref}
\SYNOPSIS
Makes {MESON} apply Plaisted's positive refinement.
\DESCRIBE
This is one of several parameters determining the behavior of {MESON},
{MESON_TAC} and related rules and tactics. When the flag {meson_prefine} is
{true}, as it is by default, Plaisted's ``positive refinement'' is used in
proof search; this limits the search space at the cost of sometimes requiring
longer proofs. When {meson_prefine} is false, this refinement is not applied.
\FAILURE
Not applicable.
\USES
For users requiring fine control over the algorithms used in {MESON}'s
first-order proof search.
\COMMENTS
For more details, see Plaisted's article ``A Sequent-Style Model Elimination
Strategy and a Positive Refinement'', Journal of Automated Reasoning volume 6,
1990.
\SEEALSO
meson_brand, meson_chatty, meson_dcutin, meson_depth, meson_skew,
meson_split_limit,
\ENDDOC
|
