Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching
We propose our work to introduce Coq into discrete mathematics teaching, allowing students to prove ZFC theorems formally. The purpose of employing Coq is to help students deepen their understanding of logical concepts rather than teaching them Coq, so we formalize the deduction system and ZFC set theory strictly following the textbook and develop several automated tactics. Students can build proofs in a textbook-style proving environment, requiring hardly any knowledge about Coq. Teaching experience shows that undergraduate students can quickly construct formal proofs of mathematical induction and Peano arithmetic using our mini ZFC theorem prover developed in Coq.
|Extended abstract (Interactive Theorem Proving in Logic Education.pdf)||375KiB|
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30
|Omnisemantics: Smooth Handling of Nondeterminism (Invited talk)|
Samuel Gruetter Massachusetts Institute of Technology
|Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching|