First-order logic and automated theorem proving - Fitting, Melvin 1942- (Springer, 1996)