As defined for use NAT-DED: is a primitive tactic.

UI-HERBRAND-TAC is a tactic for automatically applying universal

instantiation. The terms that are used are generated by finding all

subterms of the appropriate type (except quantified variables) and applying

to them all functions of the appropriate type to get all possible new terms.

I.e., you can think of it as constructing the Herbrand universe one level

at a time. The number of times that this can be done for any individual

quantified formula is controlled by the flag UI-HERBRAND-LIMIT.

© 1988-99, Carnegie Mellon University.