Raymond M. Smullyan, First-Order Logic:  Chapter V. First-Order Analytic Tableaux

Melvin Fitting FIRST-ORDER LOGIC AND AUTOMATED THEOREM PROVING. Sections 5.1 - 5.7, Section 6.1.