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
A proof starting with the line case c
followed by the assumption e : A
and terminated by the corresponding
end case c is a proof of
e : - A.
The proofs are S4-tableaux-proof of the formula given, so contain
formulas of logic S4 with the operations [] (necessary) and
<> (possible).