| Horn集上的语义正单元归结 |
| |
| 引用本文： | 李大法.Horn集上的语义正单元归结[J].清华大学学报(自然科学版),1985(2). |
| |
| 作者姓名： | 李大法 |
| |
| 作者单位： | 清华大学应用数学系 |
| |
| 摘 要： | Ｌ． Ｈｅｎｓｃｈｅｎ证明了语义归结对 Ｈｏｒｎ集是完备的［１］。但是语义归结不是正单元归结。本文的主要结果是不可满足的Ｈｏｒｎ子句集合Ｓ有这样一个反驳，对于这个反驳的每一个归结来说，或者一个祖先子句是正单元，而且该正单元在 Ｉ上是假的；或者一个祖先子句是正单元，而且从另一个祖先子句和这个归结式中删去他们的正义字后剩下的子句在 Ｉ上都是假的．其中 Ｉ是 Ｓ的任何一个解释。
|
| 关 键 词： | Horn集.归结 语义归结.正单元归结 |
Semantically - Positive - Unit Resolution for Horn Sets |
| |
| Li Dafa.Semantically - Positive - Unit Resolution for Horn Sets[J].Journal of Tsinghua University(Science and Technology),1985(2). |
| |
| Authors: | Li Dafa |
| |
| Institution: | Li Dafa Department of Applied Mathematics |
| |
| Abstract: | L. Henschen proves that semantic resolution is complete for Horn sets1].But semantie resolution is not positive unit resolution. The main result of the paper is that from an unsatisfiable Horn set S there is a refutation in which for each. resolution either one of parents is a positive unit which is false in I or a parent is a positive unit and the remaining clauses from another parent and the resolvent by deleting their positive literals are both false in I, where I is any interpretation of S. |
| |
| Keywords: | Horn sets resolution semantic resolution positive-unit resolution |
| 本文献已被 CNKI 等数据库收录！ |
