  Prime implicates and prime implicants have proven relevant to a number of
areas of artificial intelligence, most notably abductive reasoning and
knowledge compilation. The purpose of this paper is to examine how these
notions might be appropriately extended from propositional logic to the modal
logic K. We begin the paper by considering a number of potential definitions of
clauses and terms for K. The different definitions are evaluated with respect
to a set of syntactic, semantic, and complexity-theoretic properties
characteristic of the propositional definition. We then compare the definitions
with respect to the properties of the notions of prime implicates and prime
implicants that they induce. While there is no definition that perfectly
generalizes the propositional notions, we show that there does exist one
definition which satisfies many of the desirable properties of the
propositional case. In the second half of the paper, we consider the
computational properties of the selected definition. To this end, we provide
sound and complete algorithms for generating and recognizing prime implicates,
and we show the prime implicate recognition task to be PSPACE-complete. We also
prove upper and lower bounds on the size and number of prime implicates. While
the paper focuses on the logic K, all of our results hold equally well for
multi-modal K and for concept expressions in the description logic ALC.
