First-order logic and automated theorem proving - Fitting, Melvin (Text an monographs in computer science, 1990)