Standard Tableau Calculus

The standard tableau calculus extends the Propositional Tableau Calculus with the following quantifier rules:

The first rule is usually infinitely branching.