行波：数学推理的元极导航 数学推理

　　Alan Bundy,University of Edinburgy 　　David Basin,ETH Zürich 　　Dieter Hutter,DFKI Saarbrücken
　　Andrew Ireland,Heriot-watt University
　　Rippling: Meta-level
　　Guidance for Mathematical
　　Reasoning
　　2005,202pp.
　　HardcoverGBP:50
　　ISBN 978-0-521-83449-0
　　
　　A.邦迪 D.巴森等 著
　　本书是《剑桥理论计算科学专论》丛书的第56卷。自从20世纪50年代起，自动化理论证明成为一个活跃的研究领域。在该领域中的研究人员开始着手处理类似人类的自动化推理。在20世纪60年代和70年代，人们对自动化理论证明的兴趣增加了，这是由于理论进展的驱动。例如归纳的开发以及对程序验证的兴趣增加。
　　行波是数学推理自动化的一种重要的新技术。这种技术被广泛地应用于以下场合：从一个或多个相似句法结构的给定条件中证明一个结论，人们可以通过操纵调整结论而对给定条件进行充分的重组利用。这时可以对这个结论这样注释：一些子表达式可以进行修改挪动，另外一些子表达式保持原封不动；行波是许多基于公式注释的搜索控制技术中的第一种，本书的最后一章中还介绍了另外一些基于注释的推理技术。行波原本是为归纳证明而开发的，其中目标是归纳的结论，而条件则是归纳的假设。行波已被证明可以广泛应用于解决多种类型问题。从通过分析求和序列到通用的等式推理归纳的应用，这些在建立可靠的工厂系统中具有特别重要的实际意义。归纳是在重复理由所要求下进行的，无论这种重复理由是从程序循环中、递归数据结构中产生的，还是从电子线路的长期行为产生的。归纳证明不适合进行自动化推理，这是因为它的搜索控制问题，如选择归纳规则、识别辅助引理和广义推测比较困难。行波对这些问题提供了许多振奋人心的解法。一个失败的行波证明也可以从它所预期的结构来分析，这种分析将有助于实现新方案基本步骤自动化，如建立新的引理、广义化和归纳规则。
　　本书共有7章。第1章对行波的介绍；第2章各种各样的行波；第3章失效的高效应用；第4章行波的形式计算；第5章行波的作用域与限度；第6章从行波到通用的方法学；第7章结论。本书还有两个附录。附录A带注释的算法与合一算法。附录B本书中使用的函数定义。
　　本书对行波以及自动化归纳理论证明的广泛课题作了系统而又全面的介绍，它将会受到理论计算机科学专业的研究人员及研究生的欢迎。
　　胡光华，高级软件工程师
　　(原中国科学院物理学研究所)
　　Hu Guanghua, Senior Software Engineer
　　(Former Institute of Physics,the Chinese Academy of Sciences)