| 摘要: |
| 本文证明了调解法的提升引理,以及输入调解法对Horn集的完备性,进而证出了单元调解法对Horn集的完备性。 |
| 关键词: |
| DOI： |
| 分类号: |
| 基金项目:国家自然科学基金;国家教委博士点基金 |
|
| COMPLETENESS OF INPUT PARAMODULATION AND UNIT PARAMODULATION ON HORN SET |
|
Ouyang Dantong,Sun Jigui,Liu Xuhua
|
| Abstract: |
| 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. |
| Key words: |
