"WFF 'N Proof: The Game of Modern Logic" -- I found its rulebook when I recently did some housecleaning.

In summary, I wish I could recommend it, but I can't. That is because (1) it uses a formalism very different from the more usual presentations of symbolic logic and Boolean algebra, and (2) it does not try to relate its formalism to those formalisms.

WFF is short for Well-Formed Formula, and in Backus-Naur form, it is given by

<WFF> ::= <primitive> | <unary operation> | <binary operation>

<unary operation> ::= <unary operator> <WFF>

<unary operator> ::= N

<binary operation> ::= <binary operator> <WFF> <WFF>

<binary operator>::= C | A | K | E

The operators are

N = negation (not)

C = implication

A = disjunction (or)

K = conjunction (and)

E = equivalence (==)

There is no exclusive or in the game, but that is simply negation of equivalence.

They are all prefixes, in a notation sometimes called Lukasiewicz notation or Polish notation, after early-20th-cy. mathematical logician Jan Lukasiewicz. That is where "reverse Polish" gets its name -- it is suffix notation. The usual way of writing mathematical-logic formulas is prefix notation for negation and infix notation for the others: p and q, etc.

There is no discussion of truth tables in the game. These are tables of returned results for the range of function arguments. Thus, for "and", the truth table is

T = True, F = False

- F T F F F T F T

The operators have these inference rules, where o = out and i = in:

Ko: Kpq -> p, q

Ki: p, q -> Kpq

Co: Cpq, p -> q

Ci: (p -> q) -> Cpq

R: p -> (q -> p)

Ao: Apq, (p -> r), (q -> r) -> r

Ai: p -> Apq, Aqp

No: (Np -> q, Nq) -> p

Ni: (p -> q, Nq) -> Np

Eo: Epq -> Cpq, Cqp

Ei: Cpq, Cqp -> Epq

R is reiteration and repetition, a convenience in proofs.