收藏
The Little Prover - Daniel P. Friedman, Carl Eastlund

The Little Prover

Daniel P. Friedman, Carl Eastlund

出版社

The MIT Press

出版时间

2015-07-10

ISBN

9780262527958

评分

★★★★★

标签

计算机计算机科学LISP定理证明

书籍介绍
这本书与其说是教证明，不如说是让人亲历一次'证明究竟如何发生'。它不急于给出自动证明的炫技，而是用一个全手动的 rewrite 系统（J-Bob，被读者戏称'传说中的 mini Coq'），逼着你一步步看着等式如何被改写、替换、分情况展开。正因为它'简陋'，递归函数与归纳证明之间那条最核心的纽带才清晰可见：证明不是魔法，而是对每一步'为什么能这样变'的持续追问。读者反馈两极分化——有人因期待自动 prover 而失望，也有人沉迷于这种'亲手推'的踏实感。它适合对 ACL2 原理好奇、愿意慢下来理解'创造力从何而来'的人；若只想速成工具，第八章或许会让你弃坑。
AI导读
核心看点
  • 以问答体幽默讲解数学归纳法
  • 深入解析Rewrite与Induction原理
  • 配套简易证明助手辅助练习
读者共识
  • 对话风格亲切，核心概念讲解清晰
  • 构造证明需创造力，部分读者中途弃坑
  • 相比后续作品工具简陋但利于入门
精彩摘录
  • "(equal (memb? (if (equal x1 '?) (remb '()) (cons x1 (remb '())))) 'nil)"
  • "(equal (if (equal x1 '?) (memb? (if (equal x1 '?) (remb '()) (cons x1 (remb '())))) (memb? (if (equal x1 '?) (remb '()) (cons x1 (remb '()))))) 'nil)"
  • "(equal (if (equal x1 '?) (memb? (remb '())) (memb? (cons x1 (remb '())))) 'nil)"
  • "(defun add-atoms (x ys) (if (atom x) (if (member? x ys) ys (cons x ys)) (add-atoms (car x) (add-atoms (cdr x) ys))))"
  • "(add-atoms (car x) (add-atoms (cdr x) ys))"
  • "(if (< (size (car x)) (size x)) (< (size (cdr x)) (size x)) 'nil))"
  • "(if (atom x) 't (if (< (size (car x)) (size x)) (< (size (cdr x)) (size x)) 'nil))"
  • "(if (natp (size x)) (if (atom x) 't (if (< (size (car x)) (size x)) (< (size (cdr x)) (size x)) 'nil)) 'nil)"
用户评论
有点失望，原来是搞了一个全手动的rewrite system，我本来想搞自动prover的
相较于之后那本书里的 Pie，这个 J-Bob 确实简陋了些。不过简陋的好处也很明显——让读者更容易去抓住核心的概念，比如递归函数和归纳证明之间的关系。
个人觉得很一般
好喜欢里面的插画
chapter8弃坑
Explains the core idea of the ACL2 theorem prover with examples and words that are intelligible and fun to read. Now I'm a fan of "the little-" series.
The MIT Press的其他书籍查看全部

下载
收藏