[基于广义归结的自动定理证明和非经典逻辑的自动推理研究]孙吉贵

【基於广义归结的自动定理证明和非经典逻辑的自动推理研究】孙吉贵.pdf分类号C/TP31 密级内部 基于广义归结的自动定理证明 和非经典逻辑的自动推理研究 孙吉贵 指导教师 刘叙华教授 专业 计算机软件 研究方向:人工智能 论文答辩日期 授予学位日期 答辩委员会主席 论文评阅人 1993年 月Although Leibniz seventeenth-century dream ofa symiboliclamguage for the representation oiulmechanical sobition of all scienfitic and mathemotic problems has suffered at the honds of the undecidability,incomplete ness and independence results of modern mathematical logic,the spirit of his idea liv摘 要 与完备性定理.针对模态逻辑“上”型模态逻辑推论S上U.V,提出了强模态归 结推理方法,证明了强模态归结关于“卡”型模态逻辑推论的可靠性与完备性.2.将命题模态逻辑的标记归结推广到了一阶模态逻辑,提出了一种双标记 一阶模态逻辑推理方法,证明了双标记模态归结的可靠性与完备性定理.通过 反例指出:Cialdea的一阶模态逻辑归结系统的完备性结论的错误的,并给出 了,为确保系统的完备性,Cialdea归结系统的两种修正方法。:3.改进了Thistlewaite博士论文的结果,证明了:在相关逻辑LR的Gentzen 型形式系统L中,若多重集α是Ls一可证的,则存在a的L一证明r具有 Curr
———— 文字由OCR识别(未校验)，可能存在错字；请以原始完整版为准。