|Page 342 of 800||Search internet|
The quantify operator is similar to the infer and endorse operators. The quantify operator can be used for replacing lines containing the keyword 'Arbitrary'.
In the section on using lemmas in argumentations, we proved using a variant of . says whereas just says .
The problem with is that it states that the concrete meta-variable implies itself. One cannot instantiate that. To instantiate, the lemma has to have a meta-quantifier in the root as has.
Instead of proving a variant of we may also use the quantify operator:
In line L03 above, the quantify operator adds to . Then the unification tactic notes that the conclusion has a meta-quantifier in the root whereas the intended conclusion has not, and thus the unification tactic changes the argumentation to . Finally, the unification tactic uses unification to replace the ellipsis with as in
Actually, the unification tactic does double instantiation as in where is a fresh meta-variable. It does so to avoid problems when instantiating several meta-variables in parallel.
|Page 342 of 800||Search logiweb.eu|