Logic for Computer Scientists/Modal Logic/Modal Logic
Modal logic is concerned with the investigation of modalities in logics. Modalities are e.g. necessity, possibility. In classical propositional logics, propositions like "Tom is Married with Mary" may be or ; in real life however, the truth value of the above propositions obviously can change in time. In a different context the truth value may be different in different worlds: assume that Tom is dreaming about being married with Mary; hence in the world of his dreams the proposition may be true, while in real-life it may be false. In still another context, the truth value can depend whether it is considered under legal aspects: it is possible that Tom and Mary are legally married, while the catholic church is considering them to be single.
Modal logics had been studied extensively already during the first half of the 20th century by various logicians. The main breakthrough, however, was the establishment of a formal semantics of modal logic given be Kripke.
Propositional logics can be extended by modalities to describe belief, knowledge or temporal aspects. Hence it is very appropriate to use them with knowledge representation systems. Recently modal logics have been applied in verification contexts and as a means to describe the semantics of description logics.
As an example take the following puzzle:
Assume 3 children (works for children as well), who are perfect reasoners, are always truthful, and always give an answer, if they know one. The children are playing outside, and may get muddy foreheads. Any child can see if the other children have muddy foreheads, but can't see his or her own forehead. At some point, an adult says to them: at least one of you has mud on your forhead. The adult now says: Do any of you know if you have mud on your forehead. No one answers. The adult repeats the question, and again no one answers. The 3rd time the adult asks the question, one or more of the children answer. How many of the children have muddy foreheads?
This puzzle can be solved by constructing a Kripke structure, which is a set of states together with links which express the accessbility of states. There are 3 children, each can be muddy or not muddy and, hence, we have possible states. States can be represented by triples of booleans values, where a 1 in the nth position means that the nth child is muddy, and a 0 in the nth position means that the nth child is not muddy.
The Kripke structure can be defined as follows: consider, e.g. state (111). Since child 1 does not know whether or not he or she is muddy, as far as child 1 is concerned, he or she could be in state (011). For child 2 the state (011), however, is not accessible, since child 2 knows that child 1 is muddy.
A structure which is constructed as depicted above, can be used to solve the puzzle, by drawing the structure as it results after each speech action of the adult.