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 □Y using [1], where Y is a propositional knowledge base and X|=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 □Y is less than the size of the prime implicates of XΛ□Y. We have also extended the query answering algorithm in modal logic.
展开▼
