COMPLETENESS OF INPUT PARAMODULATION AND UNIT PARAMODULATION ON HORN SET
输入调解法和单元调解法在Horn集上的完备性

Here we have proved the lifting lemma of paramodulation and the completeness of input paramodulation on Horn set, and then we have also proved the completeness of unit paramodulation on Horn set.