Using sophisticated models in resolution theorem proving - Sandford, David M. (Lecture Notes in Computer Science ;, 1980)