Computing Theory Prime Implicates in Modal Logic

Abstract

The algorithm to compute theory prime implicates, a generalization of prime implicates, in propositional logic has been suggested in [9]. As a preliminary result, in this paper we have extended that algorithm to compute theory prime implicates of a modal knowledge base X with respect to another modal knowledge base (formula presented)Y]> using [1], where Y is a propositional knowledge base and (formula presented)Y in modal system T and we have also proved its correctness. We have also proved that it is an equivalence preserving knowledge compilation and the size of theory prime implicates of X with respect to (formula presented)Y is less than the size of the prime implicates of (formula presented)Y. We have also extended the query answering algorithm in modal logic.