自动推理（五）

数学中的问题解决涉及演绎和计算的相互作用，决策过程提醒人们注意两者之间的模糊划分；因此，演绎和符号系统的集成，我们在这里称之为演绎计算机代数（DCA），注定是一个富有成效的组合。 Analytica (Bauer, Clarke & Zhou 1998) 是一个建立在 Mathematica 之上的定理证明器，Mathematica 是一个强大且流行的计算机代数系统。除了提供演绎引擎之外，Analytica 还通过定义系统中缺少的许多重写规则（更准确地说，关于求和和不等式的恒等式）来扩展 Mathematica 的功能，并提供 Gosper 算法的实现，用于查找不定式的封闭形式超几何求和。配备了这些扩展知识，Analytica 可以从实际分析中半自动地证明一些重要定理，包括直接导致伯恩斯坦近似定理证明的一系列引理。以下是该定理的陈述，只是为了让读者了解我们正在处理的数学丰富程度：

伯恩斯坦近似定理。

设 I=[0,1] 为闭单位区间，f 为 I 上的实连续函数，Bn(x,f) 为 f 的第 n 个伯恩斯坦多项式，定义为 B_n(x, f)= \sum_{k=0} ^n \binom{n}{k} f(k/n)x^k(1-x)^{n-k} 然后，在区间 I 上，f 的伯恩斯坦多项式序列一致收敛于 f。

坦率地说，该程序提供了关键信息来建立导出该定理的引理，但该程序完成的演绎工作的数量和类型肯定是不平凡的。 （Clarke＆Zhao 1994）提供了使用拉马努金笔记本（Berndt 1985）第二章中的问题进行全自动证明的示例，包括邀请读者尝试的以下示例。表明：

\sum_{k=n+1}^{A_r}\frac{1}{k}=r+2\left(\sum_{k=1}^r (r-k)(\sum_{j=A_{k- 1}+1}^{a_k} \frac{1}{(3j)^3 -3j})\right) + 2r\phi(3, A_0)

其中 A_0 =1，A_{n+1}=3A_n +1 且 \phi(x,n) 是 Ramanujan 的缩写

\phi(x, n)=_{df} \sum_{K_1}^n \frac{1}{-(kx)+ k^3x^3}

Analytica 通过简化等式的左侧和右侧来证明这一恒等式，并表明两侧都简化为相同的表达式 -H_n + H_{A_r}。该简化使用了前面提到的附加求和恒等式以及谐波数的一些基本属性，

H_n=\sum_{k=1}^n\frac{1}{k}

生成的证明有 28 个步骤（其中一些步骤很重要），大约需要 2 分钟才能找到。

Kerber, Kohlhase & Sorge 1998 使用 \Omegamega 规划系统作为集成定理证明和符号计算的总体方法。在 Harrison & Théry 1998 中，我们找到了高阶逻辑定理证明系统 (HOL) 与计算机代数系统 (Maple) 集成的示例。

尽管符号代数系统功能强大，但它并没有像自动演绎系统的本质那样严格和正式。事实上，大多数代数系统中的一些知识规则的数学语义并不完全清晰，并且在某些情况下逻辑上不健全（Harrison & Théry 1998）。造成这种情况的主要原因是过于激进地不惜一切代价及时向用户提供答案，绕过对所需假设的检查，即使这意味着牺牲计算的可靠性。 （这强烈地让人想起大多数绕过所谓“发生检查”的 Prolog 实现，也以效率的名义放弃了逻辑健全性。）这个严重的问题为演绎系统为计算机代数系统提供服务提供了机会：利用其演绎能力来验证计算机代数的计算步骤是否满足所需的假设。然而，这有一个问题：对于足够大的计算步骤，验证相当于证明，并且为了检查这些步骤，推演系统很可能需要需要验证的同一系统的帮助！那么，健全性问题的解决方案可能需要对所选的符号代数系统进行广泛的修改，以使其健全；另一种方法是完全从头开始开发一个新系统，并结合自动定理证明器的开发。无论哪种情况，所得的组合演绎计算机代数系统都应显示出大大提高的自动数学推理能力。

4.4 硬件的形式化验证

自动推理已经达到了成熟的水平，定理证明系统和技术正在用于工业强度的应用。这样的应用领域之一是硬件和软件系统的形式验证。硬件缺陷的成本很容易达到数百万美元。 1994 年，奔腾处理器在出厂时其浮点单元存在缺陷，随后英特尔提出更换有缺陷的芯片（只有一小部分奔腾用户采用了这种做法），该公司因此损失了近 5 亿美元为了防止这种情况的发生，测试芯片设计的实践现在被认为是不够的，更正式的验证方法不仅在微处理器行业中获得了广泛的关注，而且已经成为一种必要。形式验证背后的想法是用数学确定性严格证明系统按规定运行。硬件设计的常见应用包括正式确定系统在所有输入上都能正确运行，或者两个不同的电路在功能上等效。

根据手头的任务，人们可以借鉴多种自动化形式验证技术，包括命题逻辑中的 SAT 求解器、使用二元决策图 (BDD) 的符号模拟、时态逻辑中的模型检查或高阶逻辑中的证明在后一种情况下，使用像 HOL 这样的自动化定理证明器（参见第 3.1 节）在实践中已被证明是无价的。像 HOL 这样的系统中的证明构造是半自动进行的，用户提供了关于如何进行证明的大量指导：用户在定理证明者的协助下尝试找到证明，根据要求，定理证明者可以自动填写证明部分或验证为其提供的证明步骤。尽管上面提到的一些技术提供了高阶逻辑所缺乏的决策过程，但高阶逻辑具有非常具有表现力的优点。这种权衡是合理的，因为证明浮点运算的事实需要大量实际分析的形式化，包括许多基本陈述，例如：

|- (!x.a <= x // x <= b ==> (f diffl (f' x)) x) //

f(a) <= K //

f(b) <= K //

(!x.a <= x // x <= b // (f'(x) = 0) ==> f(x) <= K) ==>

(!x.a <= x // x <= b ==> f(x) <= K)

Harrison 2000 在 HOL 中写的这个陈述说，如果函数 f 在区间 [a, b] 中可与导数 f' 微分，那么在整个区间内 f(x) \le K 的充分条件是 f(x) \ le K 在端点 a、b 和所有零导数点处。结果用于确定通过截断幂级数逼近超越函数时的误差界限。在这样一个“艰苦的基础系统”中进行证明（Harrison 2006）有一些显着的好处。首先，人们可以高度保证证明的有效性，因为（诚然很长）它们是由小的无错误演绎步骤组成的。其次，这些基本语句和中间结果的形式化可以在其他任务或项目中重用。例如，在证明平方根或超越函数的浮点算法的其他结果时，可以重用浮点除法的形式语句和经过验证的结果的库。为了进一步说明，英特尔安腾的不同版本的平方根算法有许多相似之处，并且一个版本的算法的正确性证明可以在对证明进行细微调整后转移到另一个版本。当然，使用 HOL 这样的证明器的第三个好处是，这种冗长的证明是机械地进行的，并且具有演绎确定性；如果是手动执行，那么引入人为错误的可能性也是肯定的。

4.5 软件的形式化验证

社会越来越依赖软件系统来提供安全和安保等关键服务。软件故障的严重不利影响包括人员伤亡、安全威胁、未经授权访问敏感信息、巨额财务损失、关键服务被拒绝以及安全风险。提高关键软件质量的一种方法是用形式验证技术来补充传统的测试和验证方法。形式验证的基本方法是生成软件必须满足的许多条件，并通过数学证明来验证（建立）它们。与硬件一样，自动形式验证（以下简称形式验证）涉及使用自动定理证明者履行这些证明义务。

安全协议的形式化验证是自动化定理证明在工业中近乎理想的应用。安全协议是小型分布式程序，旨在确保交易在公共网络上安全地进行。安全协议的规范相对较小且定义明确，但其验证却绝非易事。我们在上一节中已经提到了基于 SAT 的定理证明器在美国数据加密标准 (DES) 验证中的使用。作为另一个例子，Mondex的“电子钱包”是一种智能卡电子现金系统，最初由国家威斯敏斯特银行开发，随后出售给万事达卡国际。 Schmitt＆Tonin 2007描述了Mondex协议的Java卡实现，在该协议中以Java建模语言（JML）紧密地按照原始Z规范进行了重新重新制定安全属性。使用关键工具（Beckert，Hanle＆Schmitt 2007）进行了正确性证明，这是一种交互式定理的一阶动力学逻辑的证明环境，允许用户证明用户证明势在必行和面向对象的顺序程序的属性。用作者的话说，这种自动推理的应用证明了“有可能弥合规范和实施之间的差距，确保完全验证的结果”。

Denney，Fischer＆Schumann 2004描述了一种系统，以自动化NASA数据 - 分析航空航天软件的安全性。使用Hoare风格的程序验证技术，它们的系统生成了证明义务，然后由自动定理供体进行处理。但是，该过程尚未完全自动化，因为必须首先简化许多义务，以提高定理供者解决证明任务的能力。例如，一项这样的类别的义务对矩阵，R，在沿其对角线进行更新后需要保持对称的陈述，并具有形式：

原始形式：

\ textit {symm}（r）\ rightarrow \ textit {symm}（\ textit {diag-updates}（r））

简化形式（当r为2x2时）：

（\ forall i）（\ forall j）（0 \ le i，j \ le 1 \ rightarrow \ textit {sel}（r，i，i，j）= \ textit {sel}（sel}（r，j，i））\ rightarrow

（\ forall k）（\ forall l）（0 \ le k，l \ le 1 \ rightarrow

\ textIt {sel}（\ textit {upd}（\ textit {upd}（r，1，1，1，r_ {11}），0，0，r_ {00}），k，l）= \ textit {sel {sel} （\ textit {upd}（\ textit {upd}（r，1，1，1，1，11，r_ {11}），0，0，r_ {00}），l， k））））

即使在简化之后，当前的定理抛弃也发现了具有挑战性的证明任务。该任务对于较大的矩阵和更新的数量变得很棘手（例如，6 \ times 6矩阵，具有36个更新），并且需要在任务最终落入最先进的定理抛弃范围之内之前，需要进一步的预处理和简化义务。但是值得注意的是，在不使用定理抛弃的任何特定功能或配置参数的情况下找到证明，这将提高他们完成证明的机会。这很重要，因为定理在行业中的日常应用无法以其用户对供奉献者的深入了解。对软件的正式验证仍然是一项艰巨的任务，但是当没有自动扣除的协助下，当人们面临建立数千义务的人类不可能的任务时，就很难看到财产认证如何发生。

在核工程领域，自动推理的技术被认为足够成熟，以帮助对负责控制核电站预防核电站预防系统（RPS）的安全关键软件进行正式验证。使用NUSCR（一种为核应用定制的正式规范语言）指定了APR-1400核反应堆数字控制系统的RPS组件（Yoo，Jee＆Cha 2009）。计算树逻辑中的模型检查用于检查规格以了解完整性和一致性。之后，核工程师通过自动合成过程生成功能块设计，并使用线性时间逻辑中的模型检查技术正式验证设计；这些技术还用于验证设计的多个修订版和版本的等效性。这些模型检查工具的实施是为了使它们的使用尽可能轻松，直观，以不需要深入了解这些技术的方式，并使用了核工程师熟悉的说明。使用自动推理工具不仅有助于设计工程师建立所需的结果，而且还提高了政府监管人员的信心，这些监管人员需要批准RPS软件才能进行操作。

量子计算是物理与计算机科学交集的新兴领域。预计该领域将带来非常重要的实用应用，并且鉴于量子世界的性质，我们可以放心，不会缺乏哲学含义。这些应用需要牢固的基础，包括对量子算法的形式化和验证以及导致量子信息理论。为了实现这一有价值的目标，已经在Isabelle/Hol中正式化了许多结果，并将其添加到其图书馆中，以便可以提供进一步的工作。在对量子计算中的许多概念进行形式化之后，例如Qubit，量子状态，量子门，纠缠，测量，量子电路的矩阵表示等等，工作将继续进行定理和算法的形式化（Bordg，Lachnitt＆He 2021） ，包括：：

No-Clone定理指出，不可能做出未知量子状​​态的确切副本（Wooters＆Zurek 1982，Dieks 1982）；

量子传送协议，其形式化以前是在COQ系统（Boender，Kammüller＆Nagarajan 2015）中进行的，但现在它也是Isabelle图书馆的一部分；该协议允许在没有纠缠对和经典通道的情况下不使用量子通道的情况下传输未知的量子状态；

Deutsch算法及其广义版本Deutsch-Jozsa的算法的验证（Deutsch 1985）。德意志是第一个证明量子计算机可以比任何von-neumann-Classical-computer;和

量子游戏理论的许多结果，例如量子囚犯的困境，即古典困境的量子版本，以及不公平的量子囚犯的困境，其中一名囚犯遵守古典物理学的定律，而另一个囚犯则具有量子优势（Eisert，Wilkens＆Lewenstein 1999）。

值得注意的是，事实是，不公平的量子囚犯在伊莎贝尔/霍尔（Isabelle/hol）中形式化了原始的“纸笔”出版物中的缺陷，并且多年来未被发现。在伊莎贝尔/hol要求的更为正式和严格的框架下，发现所谓的量子“奇迹移动”（如Eisert，Wilkens＆Lewenstein 1999年所定义）比经典策略没有任何优势。现在已经纠正了此错误（Eisert，Wilkens＆Lewenstein 2020），从而重新建立了量子策略的优势。在量子计算中进一步使用isabelle/hol包括验证量子加密协议，以及伊莎贝尔库的添加量子傅里叶变换的形式化，这将为更高级的量子算法铺平道路。

4.6 逻辑与哲学

本着Wos，OverBeek，Lusk＆Boyle 1992的精神，我们提出了一个问题：关于形式逻辑和确切哲学的不同系统的以下陈述有什么共同点？

多年来，对模态逻辑S4和S5的含义片段进行了广泛的研究。作为一个空旷的问题，最终表明，有含义的S4和几个新的最短公理有一个含义S5的公理（Ernst，Fitelson，Harris＆Wos 2002）。

L组合器定义为（lx）y = x（yy）。尽管众所周知，基于l的组合器E_ {12} =（（l（ll））（l（ll）））（（l（ll））（l（ll））（l（ll）））满足e_ {12} e_ { 12} = e_ {12}问题仍然存在是否存在满足此属性的较短基于L的组合器。 （Glickfeld＆Overbeek 1986）表明，E_8 =（（ll）（l（ll）））（l（ll））是这种情况。

已经发现了经典等​​价的长度11的最短十三个公理，XCB = E（x，e（e（e（x，y），e（z，y）），z），z））是其中唯一的剩余公式长度是谁的状态不确定 - 它是公理吗？在四分之一世纪的时间里，尽管各种研究人员进行了深入研究，但这个问题仍然开放。终于解决了XCB确实是这样的单个公理，因此结束了对等效演算的最短单公理的搜索（Wos，Ulrich＆Fitelson 2002）。

坎特伯雷的圣安塞尔姆（Saint Anselm）在他的假设中提供了一个著名的上帝存在论点。但是，最近，从某种意义上说，它更短并且使用了更少的假设（Oppenheimer＆Zalta 2011）。以同样的传统，戈德尔产生了上帝存在的证明，但（Benzmüller＆Paleo 2014）最近使用较弱的逻辑系统证明了相同的结果，同时解决了对Gödel证明的主要批评。

在定义罗宾斯代数的公理中，亨廷顿的方程式 - （ - （（x + y） + - （x + -y））= x可以用更简单的一个代替，即罗宾斯方程 - （ - x + y） + - （-x + -y）= x。这个猜想一直未经证实，超过50年来抵抗包括塔斯基在内的许多逻辑学家的攻击，直到最终证明了这一点（McCune 1997）。

我们再次问，这些结果有什么共同点？答案是，在自动推理计划的帮助下，每个人都已证明了每个人。透露了这个问题的答案提示了一个新问题：在不应用这种自动推理工具的情况下解决这些开放问题需要多长时间？

模态逻辑

模态逻辑的逻辑系统S4和S5的严格影响片段分别称为C4和C5，其Hilbert-Style Axiomatizatizations以凝结的脱离为唯一的推理规则。在克里普克（Kripke）作品的洞察力中，安德森（Anderson＆Belnap）（1962）使用以下3轴基础发布了C4的第一个公理化，波兰语表示“ CPQ”表示“ P \ rightarrow Q”。

(1)

cpp \ quad ccpqcrcpq \ quad ccpcqrccpqcpr

在某个时候提出了一个问题：使用2轴的基础甚至一个单个公理，是否存在C4的这种公理化较短？作者Ernst，Fitelson，Harris＆Wos（2001）使用自动推理程序Otter，在肯定中解决了这两个问题。