針對教學場景的ZFC集合論Coq形式化

摘要： 離散數(shù)學是計算機類專業(yè)的基礎課程之一,命題邏輯、一階邏輯與公理集合論是其重要組成部分.教學實踐表明,初學者準確理解語法、語義、推理系統(tǒng)等抽象概念是有一定難度的.近年來,已有一些學者開始在教學中引入交互式定理證明工具,以幫助學生構造形式化證明,更透徹地理解邏輯系統(tǒng).然而,現(xiàn)有的定理證明器有較高上手門檻,直接使用會增加學生的學習負擔.鑒于此,在Coq中開發(fā)了針對教學場景的ZFC公理...