Algorithms For Computing Prime Implicates Using Distributivity And Labelled Resolution In Modal Logic

Abstract

"Modal Logic is used for Knowledge Representation and Reasoning in many problems. Suppose we have a knowledge Base(KB) and a Query (Q), the question here is whether KB j= Q or not. Knowledge Compilation is one of the techniques that have been proposed to deal with the computation intractability of such query answering problems. Knowledge Compilation (KC) techniques have been proposed successfully in Modal logic to overcome such logical entailment problem. So KC is split into two phases such as on-line and off-line. The KB is preprocessed in offline phase into another Knowledge Base KB0,where KB0 contains the set of prime implicates and queries are answered from KB0 in polynomial time. In this thesis, we have implemented the prime implicate computation algorithm [3] in modal logic. We have also suggested an algorithm to compute prime implicates using labelled resolution in modal logic and proved its correctness."