Raymond M. Smullyan. "First-Order Logic", Chapter II

Melvin Fitting, "Fist Order Logic and Automatic Theorem Proving", Chapter 3:  3.1 ως και 3.5