Modal logic is a kind of logic used to represent statements about necessity and possibility. It is used in computer science to reason about concepts such as uncertainty and time-dependent properties, for example in formal verification and in knowledge representation.   Many-valued logic is a logic in which there are more than two truth values. It is used, for example, to represent partial or inconsistent information in databases and in information retrieval systems.   We combine the two concepts in a general and comprehensive way. Specifically, given any finite ordered set of truth values and any set of connectives, we define two main kinds of many-valued modal logics, formulated in a certain syntax called Gentzen's sequent calculus, and prove their soundness and strong completeness with respect to certain kinds of Kripke semantics.   Additionally, we show results such as logic extensions, finite model property, strong decidability, duality via negation and relation to intuitionistic logics.  

מנחה :פרופ' אמריטוס קמינסקי מיכאל , מדעי המחשב