First-order logic and automated theorem proving - Fitting, Melvin (New York ; Berlin ; Heidelberg : Springer Verlag, 1990)