Logical connectives

& conjunction + disjunction

=> implication <=> equivalence

- negation

F faux

A proof is a sequence of proof lines.
A proof line is either a formula, the word assume followed by a formula, or the word therefore followed by a formula.
This formula is the conclusion of the proof line. Each proof line is terminated by a period.
The word assume introduces an hypothesis.
The word therefore removed the last introduced hypothesis.
A formula is usable on a proof line, if it is the conclusion of a previous proof line whose hypotheses have not been removed.

Proof Line	Effects	Conditions
assume A.	adds A to the end of the list of the hypothesis of the previous proof line	no conditions
therefore A => B.	removes the last introduced hypothesis. This proof line is the application of the rule =>I	The removed hypothesis must be A. The formula B must be usable on the previous proof line.
A.	no effects	The formula A must be a copy of a formula usable on this proof line or must be obtained by application of a rule to formulas usable on this line.

Operator priority : (high) - & + => <=> (low)
Between two identical operations, the left operation is prioritary, except for implication

A & B & C est (A & B)& C A + B + C est (A + B) + C A => B => C est A => (B => C)

A & B + C est (A & B) + C A & B => C + D est (A & B) => (C + D) - A + B est (- A) + B

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 : 29-Oct-2009