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

Ενότητα  3.3

Ενότητα  3.7