正式开始coq art

正式开始学习coq art
令人惊讶的是，居然在1970年代的SAM证明器中，就已经有了我们今天熟悉的resolution，CNF和unification。
不过unification还需要进一步探索。

哈哈，从wiki的注释看，所谓unification就是在一个lattice上，按照pre order，找共同项。