Melvin Fitting, "Fist Order Logic and Automatic Theorem Proving",

Ενότητα  4.3