A B ------ [&I] A & B	A & B ------ [&E1] A	A & B ------ [&E2] B
A ------ [+I1] A + B	B ------ [+I2] A + B	A + B A => C B => C ---------------------- [+E] C
F ---- [Efq] A	A A => B --------- [=>E] B	-- A ------- [Raa] A

The introduction implication Rule =>I is not above. It corresponds to a Proof Line begining by the Word therefore.
This rule is defined on the syntax page
The conjunction is written &, the disjonction is written +
I = introduction, E = elimination,
=>E = modus ponens,
Efq = ex falso quodlibet, Raa = reductio ad absurdum
In addition to these rules, we define the negation and the equivalence by
-A = A => F
A <=> B = (A => B) & (B => A)
In a proof, one can replace every Formula by an other Formula equal when we replace the Negations and the Equivalences by their Definitions.

examples | rules | syntax | info | download | home

Warning: date(): It is not safe to rely on the system's timezone settings. You are *required* to use the date.timezone setting or the date_default_timezone_set() function. In case you used any of those methods and you are still getting this warning, you most likely misspelled the timezone identifier. We selected 'Europe/Berlin' for 'CEST/2.0/DST' instead in /www/html/membres/michel.levy/prover/footer.inc on line 13 Last Modified : 21-Oct-2009