PAVOLJOZEF©AFÁRIKUNIVERSITYINKO©ICE
                               FACULTYOFSCIENCE
               Automated Generation of Planar
                 Geometry Olympiad Problems
                                   MASTER’S THESIS
                   Field of Study:     Informatics
                         Institute:    Institute of Computer Science
                       Supervisor:     doc. RNDr. Stanislav Krajči, PhD.
                       Consultant:     Mgr. Michal Rolínek, PhD.
            Ko¹ice 2020                                       Bc. Patrik Bak
                    Acknowledgments
         I would like to express my gratitude to: my supervisor Stanislav Krajči, for
         his support in granting me full academic freedom to pursue my own ideas;
         my consultant Michal Rolínek, whose expertise and advice took this text to
         an entirely new dimension; Pavel ©alom, for his immensely careful reading of
         the entire formal model and problem generation sections; and Dávid Uhrik, for
         countless remarks on every part of the text in terms of both content and style.
                                     Univerzita P. J. Šafárika v Košiciach
                                            Prírodovedecká fakulta
                                    ZADANIE ZÁVEREČNEJ PRÁCE
              Meno a priezvisko študenta:  Bc. Patrik Bak
              Študijný program:            Informatika (Jednoodborové štúdium, magisterský II. st.,
                                           denná forma)
              Študijný odbor:              Informatika
              Typ záverečnej práce:        Diplomová práca
              Jazyk záverečnej práce:      anglický
              Sekundárny jazyk:            slovenský
              Názov:        Automated generation of planar geometry olympiad problems
              Názov SK:     Automatické generovanie planimetrických úloh Matematickej olympiády
              Cieľ:         Design  and  implement  software  that  is  able  to  generate  planar  geometry
                            olympiad problems by extending an initial configuration with new geometrical
                            objects  and  subsequently  finding  non-trivial  theorems  in  the  generated
                            configurations.
              Literatúra:   [1] Rajiv Bagai, Vasant Shanbhogue, Jan M. Żytkow, and Shang-Ching Chou.
                            Automatic theorem generation in plane geometry. In: International Symposium
                            on Methodologies for Intelligent Systems. 1993. 415–424.
                            [2] Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A deductive
                            database approach to automated geometry theorem proving and discovering.
                            Journal of Automated Reasoning. 2000, 25 (3), 219–246
                            [3] Andreas Poulos. A research on the creation of problems for mathematical
                            competitions. Teaching of Mathematics. 2017, 20 (1)
              Vedúci:            doc. RNDr. Stanislav Krajči, PhD.
              Konzultant:        Mgr. Michal Rolínek, PhD.
              Oponent:           RNDr. Ondrej Krídlo, PhD.
              Ústav :            ÚINF - Ústav informatiky
              Riaditeľ ústavu:   RNDr. Ondrej Krídlo, PhD.
              Dátum schválenia: 02.04.2020
                                                                              
                                                  Abstract
                   We present a system that generates planar geometry problems suitable for
                   mathematical competitions such as the International Mathematical Olympiad.
                   Our solution consists of the following assets: (1) a novel, provably correct,
                   problemgeneration algorithm, (2) bulk filtering algorithms of easy problems in-
                   spired by geometry theorem proving methods, primarily the deductive database
                                                                             #
                   method, (3) a novel problem quality ranking algorithm. A C  implementation
                   of the system has been developed and made available on GitHub https://
                   github.com/PatrikBak/GeoGen.Thedevelopedalgorithmshavebeentestedin
                   manysmallandlarge-scale experiments that generated, rated, and sorted thou-
                   sands of problems, nine of which are enclosed in the appendix. Five generated
                   problems have been proposed to the International Mathematical Olympiad,
                   whilst two generated problems have already been accepted to the Czech-Slovak
                   mathematical contests.
                   Keywords: geometry problem generation, geometry theorem proving, mathe-
                   matical olympiad problems, planar geometry problems