Practice Wang's Algorithm

Here are the transformation (R1 through R5) and termination (R6 and R7) rules:

• R1: If one of the top-level formulas of a sequent has the form $\neg X$, we may
  drop the negation and move $X$ to the other side of the sequent arrow.
  Here $X$ is any formula, e.g. $P \vee \neg Q$. If the negation is to the left of the
  sequent arrow, we call the transformation "NOT on the left"; otherwise it
  is "NOT on the right".
  

• R2: If a top-level formula on the left of the arrow has the form $X \wedge Y$,
  or on the right of the arrow has the form $X \vee Y$, the connective may be
  replaced by a comma. The two forms of this rule are called "AND on the
  left" and "OR on the right", respectively.
  

• R3: If a top-level formula on the left has the form $X \vee Y$, we may replace
  the sequent with two new sequents, one having $X$ substituted for the
  occurren ce of $X \vee Y$, and the other having $Y$ substituted. This is called
  "splitting on the left" or "OR on the left".
  

• R4: If the form $X \wedge Y$ occurs on the right, we may also split the sequent
  as in Rule R3. This is "splitting on the right" or "AND on the right".
  

• R5: A formula (at any level) of the form $(X \rightarrow Y)$ may be replaced by
  $(\neg X \vee Y)$, thus eliminating the implication connective.
  

• R6: A sequent is considered proved if some top-level formula $X$ occurs
  on both the left and right sides of the sequent arrow. Such a sequent is
  called an axiom. No further transformations are needed on this sequent,
  although there may remain other sequents to be proved. (The original
  sequent is not proved until all the sequents obtained from it have been
  proved.
  

• R7: A sequent is proved invalid if all formulas in it are individual proposi-
  tion symbols (i.e. no connectives), and no symbol occurs on both sides of
  the sequent arrow. If such a sequent is found, the algorithm terminates;
  the original "conclusion" does not follow logically from the premises.