Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models

The goal of this Bachelor’s thesis is the formal specification and implementation of central theories and algorithms in the field of discrete mathematics by using the RISC Algorithm Language (RISCAL), developed at the Research Institute for Symbolic Computation (RISC). This specification language and associated software system allow the verification of specifications, by using the concept of finite model checking. Validation on finite models is intended to serve as a foundation layer for further research on the corresponding generalized theories on infinite models. This thesis results in a collection of specifications of exemplarily chosen formalized algorithms of set theory, relation and function theory and graph theory. The algorithms are specified in different ways (implicit, recursive and procedural), to emphasize the corresponding connections between them. The evaluation and validation of implemented theories is demonstrated on Dijkstra’s algorithm for finding a shortest path between vertices in a graph.