Multiple disjunctions with a Tableaux proof system I am using the Tableaux proof system, and have a question about branching and disjunctions.
Normally the example on how to use the Tableaux proof system is to get the formula to CNF, and then start branching it. It can look like this:
$$
(A \lor B), \lnot B,\lnot A
$$
And then you'd get the branches:
$A\lnot B,\lnot A$ and $B, \lnot B,\lnot A$
But sometimes I get a formula with multiple disjunctions and then I don't know if what I am doing is actually correct:
 $$
(A \lor B \lor C), \lnot B,\lnot A, \lnot C
$$
branches:
$A\lnot B,\lnot A, \lnot C$ and $(B \lor C), \lnot B,\lnot A, \lnot C$
first branch is closed, so branch second branch: $B, \lnot B,\lnot A, \lnot C$ and $C, \lnot B,\lnot A, \lnot C$
Am I doing it correctly?
 A: Short answer: yes, but note that you generally don't have CNF in tableaux. You might be thinking of resolution (where you need to do a conversion to CNF before starting out).
Ask yourself how you got to the described step. An example:
$\{(A \lor B) \land \lnot B \land \lnot A\}$ (a set of one formula) is transformed to
$\{(A \lor B), \quad \lnot B \land \lnot A\}$ (two formulae) to
$\{(A \lor B) ,\quad  \lnot B ,\quad \lnot A\}$ (three)
Here you repeatedly use the $\alpha$ rule to pick apart a single formula at a time.
Similarly, you can use $\beta$ rule to split $(A\lor B\lor C)$ one step at a time. 
Note that you need to be careful (in the sense of thinking about operator priorities) if you encounter a formula like $A\lor B \land C$.
A: Just to expand a bit on Anders's answer.
1) As he says, in applying a standard tableaux system, you don't need to process wffs by first forcing them into CNF. A standard system has a rule for "disassembling" any wff, whatever its form, depending on its main connective (or main two connectives if the first is negation). So, for example, we have the rule that says [roughly] given $\neg(A \to B)$ on a branch, add both $A$ and $\neg B$ to the branch. No pre-processing is required.
2) In standard syntaxes, $(A \lor B \lor C)$ is ill-formed, and can't appear in a formal tableau. You need $(A \lor (B \lor C))$ or $((A \lor B) \lor C)$, so the issue of multiple disjunctions in the sense of the OP doesn't arise. BUT NOTE: In Richard Jeffrey's wonderful Formal Logic: Its Scope and Limits -- which first converted so many of us to the tableaux way of doing things -- he DOES unusually allow multi-disjunctions and multi-conjunctions as primitively well-formed (i.e. not just as slang for expressions with more brackets). And in his official tableaux rules at the end of §2.1, Jeffrey deals  with multi-disjunctions and multi-conjunctions. So, for example, given $(A \lor B \lor C)$ on a branch, the rule is to split three ways, adding respectively $A$, $B$ and $C$ to the new branches. So, in headline summary, there are respectable tableaux systems which do allow multi-disjunctions and more than two-way branching of tableaux.
