一种用于自动生成证明复杂度可比的证明练习的方法
计算机科学中的逻辑
2026-03-10 v1
摘要
自动生成练习可显著减少教育者用于手动设计练习的时间。然而，要将此类自动化集成到教学实践中，最大障碍在于能够控制机械生成练习的难度。本文提出了一种用于自动生成证明复杂度可比的证明练习的方法。该方法以一个证明练习及其一组产生该练习证明的规则为输入，产生一组证明复杂度与输入练习相当的证明练习。该方法聚焦于以一阶语言表述的证明练习，涵盖通常在本科离散数学课程中涉及的主题。我们通过考虑通过非正式证明解决这些练习所需的努力来评估这些练习的证明复杂度，认为该努力可以通过无逻辑符号的 cut-based tableau 证明来正式捕获。本文引入的机制化提取程序可获得此类证明的规则。通过利用这些规则的分析性质以及通过 tableau 规则构建的证明所固有的结构，我们推导出实现所提方法的计算程序。
引用
@article{arxiv.2603.07322,
title = {A method for the automated generation of proof exercises with comparable levels of proving complexity},
author = {João Mendes and João Marcos and Patrick Terrematte},
journal= {arXiv preprint arXiv:2603.07322},
year = {2026}
}