摘要
在本文中,我们给出模态计数逻辑ML(#)在不同框架类下的可满足性的判定过程.我们使用两种方法,一种是通过修改ML(#)相对于全部克里普克框架的可满足性的判定算法,另一种是将ML(#)的可判定性归约到基本模态逻辑.我们还证明了分次模态计数逻辑GML(#)相对于全部克里普克框架的可判定性.
Abstract
In the present paper,we give the decision procedure of satisfiability of modal logic with counting ML(#)in different frame classes,by two types of methods,one by modifying the decision algorithm of satisfiability for ML(#)with respect to the class of all Kripke frames as described by J.van Benthem and T.Icard(2021),the other by reducing decidability of ML(#)to that of basic modal logic.We also show the decidability of graded modal logic with counting GML(#)with respect to the class of all Kripke frames.
基金项目
Tsinghua University Initiative Scientific Research Program()
Taishan Young Scholars Program of the Government of Shandong Province,China(tsqn201909151)
Shandong Provincial Natural Science Foundation,China(ZR2023QF021)
Support Plan on Science and Technology for Youth Innovation of Universities in Shandong Province(2021KJ086)