Title: Yet Another ZFC Set Theory Formalization in a Theorem Prover (Online)

Speaker:  Qinxiang Cao (SJTU)

Time: 15:10 ~ 18:00  (Sept. 6)

Tencent Meeting (腾讯会议) Link: https://meeting.tencent.com/dm/rzQcIrYWEpKp

Meeting ID: 657-824-601

Abstract:  

Theorem provers can check formalized definitions and proofs. Typical theorem provers like Coq, Isabelle etc. has been widely used for building up huge proofs --- topics range from logics, analysis to program semantics. But for now, users of theorem provers are mainly professionals, researchers and well-trained Ph.D students. It usually takes weeks learning to use a theorem prover. In this talk, I will introduce a new formalization of ZFC set theory in Coq. I have used it in teaching first order logic proof rules and ZFC set theory. It is designed in a way that students can easily learn how to use it, build simple formalized proof by themselves and practice directly what they have learned in class.