[自动定理证明中的RUE-NRF单元输入及锁反驳]欧阳继红

【自动定理证明中的RUE-NRF单元输入及锁反驳】欧阳继红.pdf吉林大学 硕士学位论文:自动定理证明中的RUE一NRF 单元、输入及锁反驳 专业计算机应用软件 作者欧阳继红 指导教师刘叙华教授 计算机科学系 一九八八年五月提 宴 RUE-NRF规则是用于等词关系的推理规则本文在 RUE-RRF归结的基础上定义了RUE-NRF输入归结,RUE-NRF单元归结及RUE-NRF锁归结的概念并证明了:a)对一子句集合S,若存在一从S出发的RUE-NRF输入 反驳,则一定存在一从S出发的RUE-NRF单元反驳.b)若 S为一E不可满足的单元子句集合且C为S中的一个负子句,则一定存在一从S出发以C为顶的RUE-HRF输入反驳.c)RUE-NRF输入归结在Horn集上的完备性.a)RUE-NRF锁归结的完备性本文还证明了RUE-NRF归结 的提升引理。数反身公程TR,归结和paramodulation 规则也是 完备的但不加限制引导的paramodulation 规则是 一个很弱的,不充分的规则,它的使用很快会产生大量不相关 的子句,这使得 paramodulation 的用途有限 Morris提出的正归结把互补文字归结为不等式的新取,这些不等式必须用 才能去掉.paramodulation 尽管卫归结引导了 paramodulation 过程,但 它毕竟是不完备的因为它归结到最内层不等式为了解决卫归结 归结的完备性,DIGRICOLI [《]提出了RUE-NRE NegativeReflectiveFunction)推理规则。
———— 文字由OCR识别(未校验)，可能存在错字；请以原始完整版为准。