auto

/params/

Synopsis:

/auto_params/.

Pre-conditions:

None, but the tactic may fail finding a proof if every proof is in the search space that is pruned away. Pruning is controlled by the optional params. Moreover, only lemmas whose type signature is a subset of the signature of the current sequent are considered. The signature of a sequent is essentially the set of constats appearing in it.

Action:

It closes the current sequent by repeated application of rewriting steps (unless paramodulation is omitted), hypothesis and lemmas in the library.

New sequents to prove:

None