Coq学习——《Software-Foundation》Volume1.7-IndProp IndProp We have seen several ways of writing propositions (conjunction, disjunction, and existential quantification) In this chapter, we bring yet another new tool in to the mix: inductive definition 2020-12-03 Computer Science 形式化验证 形式化验证
毕业设计安排 毕业设计安排 整理自计算机学院 2021 届本科毕业设计（论文）工作计划与校外毕设申请附件 ⭐ ：标记为学生个人需要关注 🟢 ：标记为指导老师需要关注 校外毕设申请材料 时间 内容 要求 2021 年 1 月 12 日前 ⭐ 提交校外毕设申请材料 完成外出毕业设计（论文）的申请工作 准备材料 ⭐ 保研/工作证明：（TOD 2020-12-02 Life 随笔 随笔
Coq学习——《Software-Foundation》Volume1.6-Logic Logic Coq 中的逻辑系统。 We have seen many examples of factual claims (propositions) and ways of presenting evidence of their truth (proofs). In particular, we have worked extensively with equality proposi 2020-11-30 Computer Science 形式化验证 形式化验证
Coq学习——《Software-Foundation》Volume1.5-Tactics Tactics More tactics and more properties of functional programs. how to use auxiliary lemmas in both "forward-" and "backward-style" proofs; “正推”“逆推”中使用辅助引理； how to reason abo 2020-11-30 Computer Science 形式化验证 形式化验证