|Page 91 of 800||Search internet|
Recall the proof of :
Line L01 says that follows from rule . Rule says
Line L01 comprises a label , an argumentation , and a conclusion bound together by a unification tactic .
The label is a variable. You can use arbitrary variables as labels, so feel free to name your lines or or whatever you like. The check page defines to as 100 individual variables.
Inside the proof, can be used as shorthand for the conclusion .
The unification tactic takes the argumentation and the conclusion and tries to prove the conclusion using the argumentation. The unification tactic returns an argumentation formulated as a Logiweb sequent term. At that time the conclusion has disappeared. The conclusion is merely used by the unification tactic to see what to do with the argumentation. Later on, when the proof checker evaluates the sequent term returned by the unification tactic, the proof checker will see that the sequent term indeed proves .
During proof checking, the following happens:
The unitac of knows that it is a unitac for a rule. So it first generates the Logiweb sequent operators needed for extracting the rule from the theory at hand. So now we have a proof of .
The unitac then compares with the expected conclusion and sees that it must eliminate a quantifier. Thus, it generates a suitable instance of rule :
plus a suitable instance of modus ponens:
The unification tactic uses unification to see that has to be instantiated to . Thus, the metavariable in rule is set to .
Rule says that for all object terms , , , and , the side condition endorses the conclusion . The side condition is true if is identical except for naming of bound variables to the result of replacing by in with suitable renaming of bound variables to avoid collisions. The is a meta-quantifier which quantifies over all object terms. The is an object quantifier which belongs to first order predicate calculus and Peano arithmetic.
Rule says that if one has proved and then one is allowed to conclude by modus ponens.
|Page 91 of 800||Search logiweb.eu|