AUTO-SUGGEST : MEXPR

AUTO-SUGGEST is a top-level command.
Given a completed natural deduction proof (which must
be the current dproof; use RECONSIDER to return to an old proof),
suggest flag settings for an automatic proof of the same theorem.

This will also automatically remove all uses of SUBST=
and SYM= from the proof (you will be prompted before this
happens, as it permanently modifies the proof).

This will show all of the instantiations (and primitive substitutions)
that are necessary for the proof, and suggest settings for
NUM-OF-DUPS, MAX-MATES, DEFAULT-MS, MAX-PRIM-DEPTH, MAX-PRIM-LITS
and REWRITE-DEFNS
The command format for AUTO-SUGGEST is:

 <n>AUTO-SUGGEST 

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage