根据《重庆市教育委员会关于公布2018年优秀博士、硕士学位论文名单的通知》(渝教研发[2018]4号),中心毕业生王善侠的博士论文《极小非正规时态逻辑研究》喜获2018年重庆市优秀博士学位论文。
博士论文摘要:
时态逻辑是模态逻辑的一个重要分支。随着人工智能、软件工程、模型检测等领域的产生和发展,时态逻辑在计算机科中越来越重要。本文研究的对象是极小非正规时态逻辑C2t,该逻辑是对E.J.Lemmon提出的极小非正规模态逻辑C2时态化处理后得到的。针对极小非正规时态逻辑C2t,本文从证明论、模型论和代数的角度开展了以下5个方面的创新性工作:
建立C2t的希尔伯特式公理系统HC2t。
建立C2t的加标矢列式演算系统GC2t。
建立正则模型类在时态语言下可定义的刻画定理。
建立C2t语言与一阶语言的对应理论和C2t语言的有穷模型性。
建立C2t的代数语义学。
本文开展的上述工作,从理论上丰富了现有的时态逻辑系统,并建立了一些重要的结论。这些结论在软件规约、自动定理证明和模型检测等方面都有一定的指导意义。因此本文的研究,不仅具有理论意义,而且具有应用价值。
王善侠博士简介:
2011年--2017年,于西南大学逻辑与智能研究中心攻读逻辑学博士,师从邓辉文教授。2017年获哲学博士学位,现为河南师范大学计算机与信息工程学院、软件学院副教授。