Notation:

Connectives:
->
implication
!
int negation
-<
exclusion
~
dual int negation
v
disjunction
&
conjunction
Meta-connectives:
=>
sequent turnstile
;
formula separator
Constants:
True
top
False
bottom