输入调解法和单元调解法在Horn集上的完备性

本文证明了调解法的提升引理,以及输入调解法对Horn集的完备性,进而证出了单元调解法对Horn集的完备性。