Learning-Transition-System Transition-System Description 一个六元组 \[T = (S,Act,\rightarrow,S_0,AP,L)\] \(S\), set of states \(Act\), set of actions \(\rightarrow ~ \subseteq S \times Act \times S\), 3-tuple-relation \(S_0 2020-11-02 Computer Science Model Checking Model Checking
Coq学习——《Software-Foundation》Volume1.4-Poly Poly Polymorphism Continue basic concepts of functional programming. Begin with polymoriphism. Polymorphic Lists List elements: One type -> Other types. The natlist defined in the last chap. 2020-11-02 Computer Science 形式化验证 形式化验证
《对青年数学家的建议》摘录的摘录 《对青年数学家的建议》摘录的摘录 只有平庸之辈才对自己的能力极为自信。你越强，你为自己所定的标准就越高——你能看见的工作超过自己手上研究的工作。许多未来的数学家会对于别的方向也有才能，也有兴趣，在开始数学生涯和从事其它事业之间会有艰难的抉择。伟大的Gauss曾在数学和语言学间动摇不定是出了名的，Pascal在年纪很轻时就放弃了数学而从事神学，而Descartes和Leibniz都同时以哲学家知名 2020-10-30 Life 阅读 阅读
Coq学习——《Software-Foundation》Volume1.3-Lists Lists Pair of numbers nat pair and its notation. Be care for to the format to match 1234Inductive natprod : Type :=| pair (n1 n2 : nat).Notation "( x , y )" := (pair x y). Note that patt 2020-10-28 Computer Science 形式化验证 形式化验证
Coq学习——《Software-Foundation》Volume1.2-Induction Induction Seperate Compilation Import all our definitions from the previous chapter Basics.v Require let Coq find .vo (analogous to the .class for java and .o for C) Create _CoqProject and organiz 2020-10-27 Computer Science 形式化验证 形式化验证