我给新来博士生的入门资料列表

我还不是博导，但是有一个搞硬件设计的08级博士生有意向跟我做这个方向，这跟我03年的情况多像。

这是我给他的入门资料列表

我拟了一个列表
逻辑方面
1 《LOGIC FOR COMPUTER SCIENCE>> 就在我拷给你的book/lcs.pdf,既然要搞这一行，那么基本的逻辑就要搞懂，看看有个概念就行
2 <>，这是对命题逻辑可解性的简单介绍
3 http://en.wikipedia.org/wiki/Boolean_satisfiability_problem 是wikipedia给出的SAT介绍
4 BDD是另一个重要的命题逻辑推理技术，这是wiki给出的介绍http://en.wikipedia.org/wiki/Binary_decision_diagram
5 另一个BDD的介绍，http://www.cse.iitd.ernet.in/~mbala/cs719/lectures/lect31/index.htm
6 BDD的经典论文，http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.ps
7 一阶逻辑的定理证明的一本著名的书，Logic For Computer Science Foundations of Automatic Theorem Proving，就在我给你的book/ball03all.pdf，这是后继的SMT的基础
8 SMT是结合了SAT和一阶逻辑的一种推理技术，看看wikipedia的说法，http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
9 自动机的东西就是book/lncs2500
10 高阶定理证明coq art.pdf，我这里有一个OCR的版本，来拷

编程语言，尤其是fontional programming
1 book/lambda calculus with type.pdf 是functional programming的基础
2 Practical Foundations for Programming languages，这本书讲的很全，看看，但是目前这个阶段不要强求什么都理解

软件工具
1 ocaml是一种functional 编程语言，上网去找他的完整编程环境吧。他不仅能教给你functional 的思想，本身也是一种高效的编程语言，许多形式化验证的工具都是用ocaml写的，包括大部分SMT solver， 和blast模型检测器，coq定理证明器等
2 haskell是另一种，但是太艰深了，以后再说吧