Goal-directed reasoning in clausal logic with equality. - Maximilian J. Moser (CS Press, 1996)