Formulas and proof syntax

The propositional variables are identifiers beginning with a lowercase letter, such as : a, b, p, q.
The logical connectives are :
. 
conjunction 
+ 
disjunction 

=> 
implication 
<=> 
equivalence 





The operator priority are : (high)  [] <> & + => <=> (low).
Between two identical operations, the left operation is prioritary, except for implication.
A . B . C 
is 
(A . B). C 
A + B + C 
is 
(A + B) + C 
A => B => C 
is 
A => (B => C) 
[]A=>B
 is 
([]A)=>B 

A . B + C 
is 
(A . B) + C 
A . B =>
C + D 
is 
(A . B) =>
(C + D) 
 A + B 
is 
( A) + B 
<> A + B 
is 
(<> A) + B 

To prove a formula A, we try to build a model of
 A (the negation of A) by the
given rules.
This proof attempt is a tree of branches. The main branch starts with the assumption
1:A : the state 1
of the model must satisfy the formula A.
The other branches are starting with case i
where
i is the name of the branch, and are terminating (are closed) with
end case i, when there is no model of the branch, because
there is, on this branch, an assumption e:F, that is a state
e satisfying the formula F
always insatisfiable.
Let's suppose that a branch contains the assumption e : A+B.
When applying the disjunction rule to this assumption, we are creating two branches, one with the
assumption e:A and the other with the assumption
e:B. We do the same with the disjunctive assumptions
e:(A =>B), e:(A.B), e:(A <=> B)