关于PI证明的若干注记

Some notes about PI resolving

PI证明是归结证明的一种重要类型,但是在目前所见到的文献中,对PI推理的定义还有一些不妥之处,没有确保PI推理中的每一步归结都是PI归结.文中给出了新的PI推理的定义,弥补了这一缺陷,并对PI归结的完备性定理证明所需的引理给出了两种简化证明.

PI Proving is an important type of resolution proving. But, as to the definition of PI reasoning, there are some defects in the present documents Which can′t guarantee every resolving being a PI resolving. It is proposed that a new definition of PI reasoning in order to make up for the drawback, and provide two simplified proofs of the lemma needed in the proof of the completeness of PI resoling.