Happy Khairunnisa Sariyanto

• The aim of automated reasoning is to automatically deduce information through the applica- tion of logical rules. Within this field of research, model finding aims to find a model of a given problem, i.e., a framework that evaluates all given statements to be true. Statements including quantification and modalities, such as necessity and possibility, can be formalised by logics like first-order modal logics. This master thesis presents a finite model finding method that relies on translating modal logical problems to classical logical ones to find a model that satisfies the problem or is an counterexample to the problem via an SMT solver. The method was implemented in the new finite model finder for first-order modal logic MoMo that finds Kripke-models represented in the TPTP format for Kripke-interpretation. An evaluation on problems of the TPTP problem library shows the practicality of this approach. To the best of the author's knowledge, MoMo is the first model finder for first-order modal logics.