命题逻辑中一类扩展子句消去方法

摘要

随着计算机求解问题越加复杂，问题在转化为命题逻辑子句集包含的冗余信息也越来越多，浪费计算机大量的储存空间和搜索解的时间，因此，对于冗余信息的删减有助于提高计算机求解问题的效率．针对命题逻辑子句集化简问题，在原有冗余性质P、RP基础上，提出多种扩展的、具有性质HRP、ARP的子句消去方法，并通过将不对称文字添加前置方法与命题逻辑集合封锁(SET_BC)、蕴涵模归结原则（IMR）结合，分别提出不对称集合封锁(ASET_BC)消去方法和不对称蕴涵模归结（AIMR）原则．最后，提出L-集合蕴涵模归结(L-SET_IMR)原则和L-不对称集合蕴涵模(L-ASET_IMR)原则．所提出的方法丰富了命题逻辑中冗余性子句消去理论和方法．

关键词

命题逻辑 / 可满足性 / 冗余性 / 不对称集合封锁 / 不对称蕴涵模归结原则 / L-集合蕴涵模归结

基金资助

国家自然科学基金（61976130和62106206）; 四川省科技计划项目（2020YJ0270）