Title: Knuth-Bendix completion of Horn clause programs for restricted linear resolution and paramodulation