UNIFORM-SEARCH : MEXPRUNIFORM-SEARCH is a top-level command.
Enter the test top level to search for any mode that will prove
a given theorem. The mode provided by the user should list flag settings
that are not to be varied, and the searchlist provided by the user should
list all of the flags to be varied. The default settings for the mode and
searchlist are UNIFORM-SEARCH-MODE and UNIFORM-SEARCH-2.
If you opt for the searchlist to be automatically modified, TPS will inspect
the given wff to check whether it is first order, whether it contains any
definitions, whether it contains any equalities (and if so whether the LEIBNIZ
and ALL instantiations are different), and whether it has any possible primitive
substitutions, and will then remove or modify any unnecessary flags from the
searchlist (respectively, unification bounds will be deleted, REWRITE-DEFNS will
be deleted, REWRITE-EQUALITIES will be deleted or modified, and DEFAULT-MS will
be changed to a search without option sets).
Also, if you opt for the searchlist to be modified and there is a proof of this
theorem in memory, AUTO-SUGGEST will be run and you will be asked whether to
modify the searchlist using the results it provides.
After entering the test top level with this command, type GO ! to start
searching for a successful mode.
The command format for UNIFORM-SEARCH is:
<n>UNIFORM-SEARCH GWFF WINDOW MODE SLIST MODIFY
"GWFF0-OR-LABEL-OR-EPROOF" "YESNO" "SYMBOL" "SYMBOL" "YESNO"
The arguments have the following meaning:
GWFF : Gwff or Eproof
WINDOW : Open Vpform Window?
MODE : Mode
SLIST : Searchlist
MODIFY : Automatically modify searchlist?
TPS documentation homepage