|Page 333 of 800||Search internet|
The instantiation operator allows to instantiate a meta-variable explicitly. After adaption the conclusion of must have a meta-quantifier as principle operator.
Explicit instantiation is handy in situations where unification gives an Incomplete unification. Uninstantiated variable: x error message. The multzero proof provides a good example in Line L09:
Unification is unable to guess from and that is the induction variable. Such guessing is possible but requires more intelligence than unification provides. Thus, the induction variable has to be given explicitly.
|Page 333 of 800||Search logiweb.eu|