| 命题逻辑中一类扩展子句消去方法 |
| |
| 引用本文： | 刘凌荣,陈树伟,吴贯锋.命题逻辑中一类扩展子句消去方法[J].四川师范大学学报(自然科学版),2023(1):117-124. |
| |
| 作者姓名： | 刘凌荣 陈树伟 吴贯锋 |
| |
| 作者单位： | 1. 西南交通大学数学学院;2. 系统可信性自动验证国家地方联合工程实验室 |
| |
| 基金项目： | 国家自然科学基金（61976130和62106206）；;四川省科技计划项目（2020YJ0270）； |
| |
| 摘 要： | 随着计算机求解问题越加复杂，问题在转化为命题逻辑子句集包含的冗余信息也越来越多，浪费计算机大量的储存空间和搜索解的时间，因此，对于冗余信息的删减有助于提高计算机求解问题的效率．针对命题逻辑子句集化简问题，在原有冗余性质P、RP基础上，提出多种扩展的、具有性质HRP、ARP的子句消去方法，并通过将不对称文字添加前置方法与命题逻辑集合封锁(SETBC)、蕴涵模归结原则(IMR)结合，分别提出不对称集合封锁(ASETBC)消去方法和不对称蕴涵模归结(AIMR)原则．最后，提出L-集合蕴涵模归结(L-SETIMR)原则和L-不对称集合蕴涵模(L-ASETIMR)原则．所提出的方法丰富了命题逻辑中冗余性子句消去理论和方法．
|
| 关 键 词： | 命题逻辑 可满足性 冗余性 不对称集合封锁 不对称蕴涵模归结原则 L-集合蕴涵模归结 |
|
