一个L_(m4c)意图后承的判定算法

A DECISION ALGORITHM BASED ON L_(m4c)

本文将提出一个基于 Lm4c的意图后承判定算法 ,即输入任何命题公式 φ、ψ,判断 φ→ ψ在 Lm4c中是否成立 .在变元较多的情况下 ,完全根据语义来判断意图后承的方法会使时间复杂度大得令人无法接受 ,因此 ,我们采用了语法、语义相结合的手段 :用分析形式结构的方法排除多数情况 ,对剩余的从形式结构不好处理的少量情况再用语义检测 .算法的最坏时间复杂度仍然是指数量级的 ,但出现最坏时间复杂度的概率被压缩到非常小的水平 ,因而平均时间复杂度相当好 .我们还将给出实验结果 。

In this paper we propose an algorithm based on L m4c to decide intention consequences. For anyφ?ψ,it can decide whether φ→ψ holds in L m4c .With a large number of atoms,the complexity of the computation will become intractable if it only relies on semantics,so the introduction of syntactic analysis is necessary.In our algorithm,we did combine them together.The worst case time complexity of the algorithm still has a exponential magnitude,but the average time complexity is pretty good because the probability of the worst cases is very small.Finally,we give the proof of the correctness of the algorithm and the result of experiments.