Modal logic is a branch of mathematical logic studying mathematical models of correct reasoning which involves various kinds of necessity-like and possibility-like operators. The first modal systems were created in the 1910s and later by Lewis (cf. Lewis and Langford, 1932) who used the operators "it is necessary" and "it is possible" for analyzing other logical connectives, in particular implication. Orlov 1928) and Godel 1933) constructed modal systems with the operator "it is provable" and exploited them to interpret Heyting's intuitionistic logic. More recently numerous modal systems have originated from different sources.