基于归结的模态逻辑中主蕴涵计算算法
计算机科学中的逻辑
2019-03-26 v2
摘要
本文提出了一种利用Enjalbert等人所提归结方法计算K中模态公式主蕴涵的算法。本文所提算法计算主蕴涵的时间为多项式乘指数时间，即O(n^{2k}×2^{n})，而Binevenu的算法计算主蕴涵需要双指数时间。我们还证明了其正确性。
引用
@article{arxiv.1811.04566,
title = {An Algorithm for Computing Prime Implicates in Modal Logic Using Resolution},
author = {Manoj K. Raut},
journal= {arXiv preprint arXiv:1811.04566},
year = {2019}
}