Prime Implicates and Prime Implicants in Modal Logic

Abstract

The purpose of this paper is to examine how the propositional notions of prime implicates and prime implicants might be appropriately extended 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 which perfectly generalizes the propositional notion, 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 this definition. To this end, we provide sound and complete algorithms for generating and recognizing prime implicates, and we prove the prime implicate recognition task to be Pspace-complete. While the paper focusses on the logic K, all of our results hold equally well for multi-modal K and for concept expressions in the description logic ALC. 1