Book

First-order logic and automated theorem proving

by Melvin Fitting