UI-HERBRAND-TAC is a tactic.
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.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage