通过有限模型的自动检验开展数学理论与算法形式化教学
计算机科学中的逻辑
2018-03-06 v1
摘要
在逻辑与证明的实际应用（如计算机程序的形式化规约与验证）教学中，一个实质性障碍在于：投入于证明的大部分时间与精力实则徒劳无功——由于学生所开发的规约或算法中存在错误，其证明尝试往往毫无意义（因所证命题实则无关紧要）或注定失败（因待证命题实则不成立），这常引发挫败感并败坏形式化方法的声誉。RISCAL（RISC Algorithm Language）是一种形式化规约语言及配套软件系统，试图通过让逻辑形式化变得有趣而非负担来克服此问题。为此，RISCAL 允许学生通过在（小规模）有限模型上自动求值/执行并检验命题或算法的实例，轻松验证其正确性。从而许多/大多数错误可被迅速发现，后续的证明尝试可聚焦于更/最可能既有意义又为真的命题。
引用
@article{arxiv.1803.01472,
title = {Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models},
author = {Wolfgang Schreiner and Alexander Brunhuemer and Christoph Fürst},
journal= {arXiv preprint arXiv:1803.01472},
year = {2018}
}
备注
In Proceedings ThEdu'17, arXiv:1803.00722