|Page 95 of 800||Search internet|
Recall the proof of :
Line L06 references Lemma which says:
The unification tactic instantiates , , and to , , and , respectively. The instantiation is 'parallel': first , , and are instantiated to three fresh variables, and then those three fresh variables are instantiated to , , and , respectively. That is necessary to avoid problems when , , and are replaced by terms which may themselves contain , , and .
The unification tactic uses the conclusions of L04, L05, and L06 to guess the values for , , and . If you make a bug, unification may be unable to find values for variables, and then you get an error message from the unification tactic.
The term denotes where is modus ponens of the object theory and is the meta modus ponens operator of the Logiweb sequent calculus. Thus, denotes modus ponens in the object theory and denotes meta modus ponens. Several concepts have versions both in the Logiweb sequent calculus and in :
|Operation||Meta level||Object level|
|Page 95 of 800||Search logiweb.eu|