CAJ | 학술논문

为了近一步提高模态逻辑推理机的效率,提出了两种Tableau算法优化技术——冲突技术和矛盾学习技术,并结合这两种技术实现了针对模态逻辑S4的推理机S4P.在此基础上,为了从Tableau算法生成的模型图中构造一个规模较小的模型,又提出通用模型的概念,然后给出通用模型的规约技术并证明该技术对于任意依赖于公理D、T、B、4和5中部分或全部公理的正规模态逻辑的正确性.最后,使用逻辑工作台测试用例对S4P的效率进行测试,实验结果表明S4P的效率优于RACER和FaCT++;同时,对S4P生成的测试用例中非有效公式的否定对应的通用模型进行规约,实验结果表明通过模型规约能明显地缩减模型的规模.
위료근일보제고모태라집추리궤적효솔,제출료량충Tableau산법우화기술——충돌기술화모순학습기술,병결합저량충기술실현료침대모태라집S4적추리궤S4P.재차기출상,위료종Tableau산법생성적모형도중구조일개규모교소적모형,우제출통용모형적개념,연후급출통용모형적규약기술병증명해기술대우임의의뢰우공리D、T、B、4화5중부분혹전부공리적정규모태라집적정학성.최후,사용라집공작태측시용례대S4P적효솔진행측시,실험결과표명S4P적효솔우우RACER화FaCT++;동시,대S4P생성적측시용례중비유효공식적부정대응적통용모형진행규약,실험결과표명통과모형규약능명현지축감모형적규모.