ABSTRACT
G system proofs may be constructed in either of the two normal forms described earlier: proof normal form and refutation normal form. The first of these approaches places formulas in the succedent position then endeavours to falsify the formula and thus the sequent. A deduction tree in which each branch terminates with an axiom, a valid sequent, is sufficient to prove the original formula valid. Refutation normal form, on the other hand, places a negation normal form of the negated formula in the antecedent then systematically attempts to satisfy the formula and thus the sequent. A deduction tree in which each branch terminates with an axiom now indicates contradiction and indirectly shows the validity of the original unnegated proposition.
