归结原理是自动推理中一种简洁、可靠且完备的推理规则。基于矛盾体分离的自动演绎理论是归结原理的延伸，矛盾体是该理论的核心部分。由于矛盾体结构复杂且生成策略较少，因此本文提出了一种新的生成矛盾体的策略，即利用多个标准矛盾体生成文字块矛盾型，再通过添加互补矛盾集得到新的矛盾体。重点讨论了具有特殊结构的文字块矛盾型生成的矛盾体，即子句正则矛盾体的性质，这些性质说明了具有特定结构的子句正则矛盾体添加子句后仍然是矛盾体。最后，提出了矛盾体的生成算法，为在计算机上实现新的矛盾体的生成提供参考。
科研之友
微信
新浪微博
Facebook
分享链接
