Page 91 of 800
| 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:
from the check page on the multzero page.
and 
where the latter is the Logiweb proof checker. tactic expands each proof into Logiweb sequent terms and then evaluates the sequent terms to see what they prove.
invokes the tactics of each construct of the proof. Among other, when it sees the construct in Line it invokes the unification tactic., the unification tactic unitac expands the argumentation with the goal of proving .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 |