证明与计算(3): 二分决策图(Binary Decision Diagram, BDD)

0x01 布尔代数(Boolean algebra)

大名鼎鼎鼎的stephen wolfram在2015年的时候写了一篇介绍George Boole的文章：George Boole: A 200-Year View。

怎样用数学公理重新表达经典逻辑？George Boole在19世纪的时候开始思考这件事，在他的书《The Mathematical Analysis of Logic》里面George Boole首次展示了使用符号加运算符的方式表示逻辑，例如“And”是“xy”，“NOT”是“1-x”，“OR”是“x+y-2xy”。但是x^2是什么呢？命题x加上命题x还是命题x，George Boole又规定了x^2=x。在George Boole的另一本书《An Investigation of the Laws of Thought》里面，Gerge Boole认为自己在发明一个“science of intellectual powers”，区别于牛顿发明微积分是“physical science”。

从George Boole开始，在经过Frege, Peano, Hilbert, Whitehead, Russell, Gödel 和 Turing等一系列数学家/计算机科学家的工作后，直到克劳德·香农( Claude Shannon )才开始让布尔代数实用。

“这个过程是必然会发生的么？”stephen wolfram思考到。布尔代数的历史显示了一个从复杂问题中慢慢产生的简单的形式化思想，偶然间就被大规模使用了