软件学报

作者：李静，欧阳丹彤，叶育鑫

单位：李静，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001211,欧阳丹彤，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001202,叶育鑫，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001203

关键词：公理定位;后继式判定算法;定位规则;白盒与黑盒

基金：国家自然科学基金（42050103，62076108）

公理定位能够挖掘描述逻辑中可解释的缺陷，并为逻辑蕴含结果寻找隐藏的理由，因此在描述逻辑研究中引起了广泛的关注.平衡描述逻辑表达能力和推理机求解效率问题一直是公理定位研究的重点内容.基于一种后继式判定算法，从白盒和黑盒两个角度将其用于公理定位.白盒方法利用修正的后继式规则（即定位规则）来追踪推理的具体过程，并引入定位公式的概念建立子句的布尔公式标签与逻辑蕴含的所有极小公理集之间的对应关系.黑盒方法则直接调用基于未修正的后继式规则的推理机，并进一步利用碰集树方法求得逻辑蕴含的所有理由.最后，基于这样的两种面向强表达描述逻辑本体的公理定位算法设计推理工具，从理论和实验两方面验证其可行性，并与已有的推理工具比较求解性能.

来源：2023年第8期

《软件学报》期刊编辑部

查看软件学报杂志2023年第8期