【非经典逻辑的自动推理及约束可满足问题研究】刘瑞胜.pdf
博士学位论文 非经典逻辑的自动推理 及约束可满足问题研究 刘瑞胜 吉林大学计算机科学系 一九九七年五月
(Ph.D.Dissertation) Automated Reasoning in Non-Classical Logic and Constraint Satisfiability Problems Ph.D.Candidate LIU Ruisheng Supervisor LIU Xuhua JIANGYunfei Speciality ComputerSoftware DepartmentofComputerScience JilinUniversity May
本文讨论了知识和信念的本质,阐述了其认识论背景,建立了关于知识和信 念的可靠和完备的模态逻辑系统,并将其推广到了多认识主体的情形。本文还使 用语义tableau方法建立了认识逻辑的证明理论,阐述了认识逻辑的可判定性.本文对认识逻辑又做了进一步推广,讨论了在认识模型下的非单调推理。非单调 推理是在单调的逻辑框架下进行的,非常灵活,而且有很强的表达能力.本文还讨论了模态逻辑的标记模态归结方法,将其分别推广到K,K4,D4,T和S4命题模态逻辑系统,证明了其可靠性和完备性。