A method for the automated generation of proof exercises with comparable levels of proving complexity

TL;DR

This paper introduces a method to automatically generate proof exercises with similar difficulty levels by analyzing and replicating the proving complexity of initial exercises, aiding educators in creating consistent problem sets.

Contribution

The paper presents a novel automated approach to generate proof exercises with controlled complexity using tableau proof analysis and rule extraction, specifically for undergraduate discrete mathematics.

Findings

Successfully generates exercises with comparable proving complexity

Uses cut-based tableau proofs to measure effort required

Provides a mechanizable procedure for exercise generation

Abstract

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.