Page 314 of 800
| Page 314 of 800 | Search internet |
T proof of L : P
has a companion
proof of L : P
which we shall refer to as the plain proof constructor.
The plain proof constructor tactic evaluates 
in order to prove 
. Tactic evaluation is similar to macro expansion and rendering.
The T proof constructor uses the tactic definition of 
to prove . Thus, the T proof constructor allows to customize tactic evaluation on a per theory basis whereas the the plain proof constructor treats all proofs equally.
As an example of a proof which uses the plain construct, consider the following proof of Lemma 1.8 in Mendelson: 'Introduction to mathematical logic'.
In Line 
we assume propositional calculus 
as defined on the Peano page.
In Line 
we use Axiom 
of to prove 
. Line 
and 
are similar.
In Line 
we apply Modus Ponens 
of to Line 
and to conclude 
. Line is similar.
| Page 314 of 800 | Search logiweb.eu |