A method for the automated generation of proof exercises with comparable levels of proving complexity
This method aims to reduce the time educators spend on manually designing proof exercises by automating the generation process while controlling difficulty, which is a problem for educators teaching Discrete Mathematics.
This paper introduces a method for automatically generating mathematical proof exercises with comparable levels of proving complexity, focusing on first-order logic problems in undergraduate Discrete Mathematics. The method takes an existing exercise and a set of proof rules as input, then outputs new exercises with similar complexity, assessed by the effort required for informal proofs captured through cut-based tableau proofs.
The automated generation of exercises may substantially reduce the time educators devote to manual exercise design. A major obstacle to the integration of such automation into teaching practice, however, lies in the ability to control the difficulty of mechanically generated exercises. This paper presents a method for the automated generation of proof exercises with comparable levels of proving complexity. The method takes as input a proof exercise together with a set of rules that yield a proof of the exercise, and produces as output a set of proof exercises whose proving complexity is comparable to that of the input exercise. The approach focuses on mathematical proof exercises formulated in first-order languages, covering topics typically addressed in undergraduate Discrete Mathematics courses. We assess the proving complexity of these exercises by considering the effort required to solve them through informal proofs, and argue that this effort can be formally captured through cut-based tableau proofs that are free of logical symbols. The rules governing such proofs are obtained through a mechanizable extraction procedure introduced in this paper. By exploiting the analytic nature of these rules and the structure inherent in proofs constructed via tableau rules, we derive a computational procedure implementing the proposed method.