English

An Algorithm for Computing Prime Implicates in Modal Logic Using Resolution

Logic in Computer Science 2019-03-26 v2

Abstract

In this paper we have proposed an algorithm for computing prime implicates of a modal formula in K\mathbf{K} using resolution method suggested in \cite{Enjalbert}. The algorithm suggested in this paper takes polynomial times exponential time ,i.e, O(n2k×2n)O(n^{2k}\times 2^{n}) to compute prime implicates whereas Binevenu's algorithm \cite{Bienvenu} takes doubly exponential time to compute prime implicates. We have also proved its correctness.

Cite

@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}
}
R2 v1 2026-06-23T05:12:13.961Z