Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models

Wolfgang Schreiner, Alexander Brunhuemer, Christoph Fürst

Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most…