代换定理的证明及其应用

Proof of the Substitution Theorem and Its Application

本文给出了代换定理的优于文献[1]的证明方法,并把代换定理与其他定理结合,构造了一个判定DNF表达式永真性的算法,使代换定理得到实际应用。

In this paper the proof and application of the substitution theorem are studied, which play an important role in deciding DNF expression validity. A new concise proof method is given and an algorithm of practical significance for deciding the DNF expression validity is constructed by combining the substitution theorem with the clause-elimination theorem and the subsumption rule. The algorithm described can speed up the decision of the DNF expression validity.