針對(duì)教學(xué)場(chǎng)景的ZFC集合論Coq形式化

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