Title: A resolution-based theorem prover
First published: 1983