"A Database-Complete Proof Procedure Based on SLD-Resolution."

Laurent Vieille (1987)
a service of  Schloss Dagstuhl - Leibniz Center for Informatics