欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
为了近一步提高模态逻辑推理机的效率,提出了两种Tableau算法优化技术——冲突技术和矛盾学习技术,并结合这两种技术实现了针对模态逻辑S4的推理机S4P.在此基础上,为了从Tableau算法生成的模型图中构造一个规模较小的模型,又提出通用模型的概念,然后给出通用模型的规约技术并证明该技术对于任意依赖于公理D、T、B、4和5中部分或全部公理的正规模态逻辑的正确性.最后,使用逻辑工作台测试用例对S4P的效率进行测试,实验结果表明S4P的效率优于RACER和FaCT＋＋;同时,对S4P生成的测试用例中非有效公式的否定对应的通用模型进行规约,实验结果表明通过模型规约能明显地缩减模型的规模.
英文摘要：
In this paper,two new techniques about optimizing Tableau algorithm are proposed.Based on them and some other techniques proposed previously,a Tableau based modal logic S4 prover called S4P is implemented.Furthermore,in order to construct a model with smaller size from the model graph which is generated by Tableau algorithm for a satisfiable modal formula,a new concept called general model and a new technique about reducing the general model are proposed.Then this paper proves the soundness of the reducing technique for any normal modal logic depending on one axiom or some axioms from D,T,B,4 and 5.Finally,S4P is tested on the Logic Work Bench （LWB） benchmarks.The experimental results show that S4P is superior to RACER and FaCT＋＋ for most problems.For the negation of the invalid formulae in the LWB benchmarks,this paper also uses the reducing technique to simplify the general models generated by S4P.The experimental results show that the new technique can obviously reduce the sizes of models.
同期刊论文项目
同项目期刊论文
期刊信息
位置：