Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
meson_prefine : bool ref
SYNOPSIS
Makes MESON apply Plaisted's positive refinement.
DESCRIPTION
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 CONDITIONS
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.