Um método para geração automatizada de exercícios de demonstração com um nível de complexidade similar

Abstract

The automated generation of exercises may benefit educators by significantly reducing the time they spend in manually creating exercises. However, an obstacle in making such automation more present in an educator’s professional routine is controlling the level of complexity of mechanically generated exercises. In this work, we present a method for the automated generation of proof exercises with a comparable level of complexity. The inputs of this method are a proof exercise and a set of rules allowing to prove this exercise. The output is a set of proof exercises with a comparable complexity to that of given as input. The scope of exercises we work with are mathematical proof exercises described in first-order languages, covering topics such as Set Theory and Number Theory. In order to calculate the level of complexity of these exercises, we base our approach on the effort required to solve them via informal proofs. We argue that such an effort, in turn, may be captured by formal proofs in cut-based tableaux that do not contain logical symbols. The rules utilized in these proofs are extracted by a mechanizable procedure we provide. We use the analytic character of such rules and the formal structure tableau proofs have to provide a computational procedure of the method in question. As case studies, we demonstrate how our method works with fragments of Set Theory and Number Theory. A prototype implementation of the method was also developed and we present it here.