In this thesis we examine one of the methods of acquiring a model for logical formulae known as tableaux. We are interested in it because of an algorithmic approach with which it can be described and easily transferred to a computer. Special attention is given to describing said method for a particular type of logic known as modal logic. The thesis consists of four chapters. In the first chapter we are introduced to the syntax and semantics of basic modal language. We highlight the similarities and differences with propositional logic, especially in the definition of truth. Great care is taken to explain modal operators as they play an essential part of the basic modal language. The end of first chapter states the goal of this thesis: providing an effective algorithm for finding a model in which a formula of the basic modal language is satisfiable. Moreover, we give a link between the concept of satisfiability and validity of formulae and conclude the effectiveness of our algorithm for finding both. Second chapter begins with a classification of formulae to relevant groups. This approach was first introduced by Smullyan in [8]. He uses \(\alpha\) and \(\beta\) classes of formulae that we denote slightly different, albeit the main concept stays the same. We continue by introducing the rules of the tableaux method for propositional logic and other basic concepts needed. We emphasize that these rules are strictly syntactic in nature. The semantic meaning follows at the end of the chapter from the proof of two very important theorems: soundness and completeness. Soundness of the tableaux method links the concept of closed tree and unsatisfiability of formulae of which said tree is built from, moreover, it follows that if a formula has a closed tree, then it is unsatisfiable. Completeness gives us the converse: for an unsatisfiable formula all trees must close. This result gives us the freedom to use the syntactic rules of the algorithm, for example on a computer, and the implied semantic meaning stays with it. Third chapter expands our classification by one more class, and that is successor formulae. This class consists of all formulae built by applying a modal operator on some formula of the basic modal language and their negations. We introduce the concept of expanded closure and we prove that it is finite. Continuing on, we state a modified tableaux method from chapter two and show its drawbacks. We state the rules of a new tableaux method that will strive to fix the drawbacks mentioned earlier. The tableaux method from chapter two is an integral part of our new method. As such, understanding of concepts in chapter two is imperative for the proper understanding in chapter three. As in chapter two, these rules are syntactic in nature and easily transferable to a computer. The continuation of chapter three consists of the proof of soundness and completeness of our new method for basic modal language. Important concepts to remember are Hintikka structures and labelled graphs. By concluding these proofs we have given a link between the syntactic rules and semantic meaning, but for a more complicated, basic modal language. Chapter four deals with the question of decidability. We state what a Turing machine and Turing-decidability are. We then proceed to show that both of the problems solved by the methods examined here are decidable in contrast to the same problem in first order logic which is not decidable. Finally, I would like to thank my mentor, assist. prof. Tin Perkov for his boundless patience and a variety of suggestions that have made this thesis possible. Furthermore, I would also like to thank my co-mentor, assoc. prof. Mladen Vuković, for very interesting lectures that made me want to expand my knowledge of logic, without which this thesis would not be possible.