Automated theorem proving : A LOGICAL BASIS - Loveland, Donald W. (North-Holland Publishing Company, 1978)