The purpose of this paper is to extend the notions of prime implicates and prime implicants to the basic modal logic K. We consider a number of different potential definitions of clauses and terms for K, which we evaluate with respect to their syntactic, semantic, and complexity-theoretic properties. We then continue our analysis by comparing the definitions with respect to the properties of the notions of prime implicates and prime implicants that they induce. We provide algorithms and complexity results for the prime implicate generation and recognition tasks for the two most satisfactory definitions.
Subjects: 11. Knowledge Representation; 3. Automated Reasoning
Submitted: Apr 24, 2007