【基於重写规则法和广义单元归结原理的定理证明系统】刘广清.pdf
吉林大学硕 士学位论文 基于重写规则法和广义单元归结 原理的定理证明系统 专业:计算机应用 刘广清 指导教师:刘叙华教授 计算机科学系 一九八九年五月
公式的两种内部表示形式(SkoLem化过程 FL与RFL模块 输出过程 第五章实例分析 第一节一个例子 第二节FL与RFL的比较 结论 致谢 参考文献
80年代初,Hsiang等人不仅成功地把重写规则法用在命 题逻辑上,而且进一步推广到一阶逻辑上,并建立了使用量写规 则的定理证明系统TeSRe,实验表明:这种证明系统所产生的新 项数比使用归结法所产生的归结式数或是自然推导法所产生的目 标数要少得多.80年代后期,要云飞副教授在布尔代效标准重写系统的基 础上,提出一套把一阶逻辑公式转换成布尔环等式的转换规则及 化简规则,并由此建立了一阶逻辑的重写证明算法F工,这种算 法可以充分地利用环上的因子分解,证明过程中产生的中间等式 也显著减少,对包含蕴涵符号或等价符号的一阶公式尤为使利 本文是对F工算法的进一步加细与深化,提出了广义单元归 结原理并给