The basic modal language extends the alphabet of the propositional logic using a modal operator of possibility \(\lozenge\). Although they share syntax similarity with propositional logic, modal logics are basically fragments of first- and second-order logics. That implies the question of their decidability. The main goal of this work is to prove that a lot of normal modal logics are decidable using their finite model property. In the first chapter we describe the fundamentals of the basic modal language syntax and semantics. A normal modal logic is a set of basic modal language formulas which are generated from the axioms using rules of proof. The smallest normal modal logic is K. Its extensions are created by adding more axioms. In the second chapter we prove that the basic modal language has the finite model property. That means that every satisfiable formula of the basic modal language is satisfiable on some finite model. Many normal modal logics have the finite model property. We prove that by using two di erent methods: selection and filtration. We observe the finite frame property as well because frames are more suited for showing the validity of formulas. Lastly, we prove the equality between those two properties. In the final chapter we explain the manner in which we represent modal logic on the tape of a Turing machine. We introduce two strategies for proving the decidability of logics. They di er by the way the logic is specified: semantically as the logic of some class of frames or syntactically by axioms. Both strategies are based on the finite model property and they hand results for many known modal logics including all extensions of logic S4:3.