自动验证的(0,S,=)逻辑片段BDD表示及验证算法

本研究论文深入探讨了自动验证无量化的第一阶逻辑（FOL）中零、后继者（S）和相等性的片段在布尔代数中的应用。具体关注的是这些逻辑表达式的布尔组合，即由变量0和后继操作符S构建的等式。研究的焦点在于使用决策图，尤其是二元决策图（BDD）和有序BDD（OBDD）来表示和验证这些公式。 作者提出了一个（0,S,=）-BDD表示法，这是一种特殊的BDD表示形式，用于表示这些特定理论中的逻辑公式。BDDs作为一种图形工具，能够有效地处理布尔函数，特别在验证命题逻辑中的公式方面展现价值。在BDD方法中，一个布尔函数被认为是可满足的，当且仅当其唯一的OBDD表示没有对应的值为0的状态。 论文的核心贡献在于引入了一个（完全）项重写系统，它能将任意给定的（0,S,=）-BDD转换为等价的有序BDD。这个有序BDD表示的优势在于，可以通过常数时间来验证原始公式，提高了效率。此外，作者还设计了一个算法，自动化这一转换过程，使得复杂度得以控制，适用于实际的自动验证需求。 该工作对于理论计算机科学领域，特别是在软件工程系的自动验证任务中具有重要意义，因为它提供了一种有效的方法来处理和验证具有零、后继和相等性的FOL公式，这对于硬件设计验证和符号模型检查等领域具有实用价值。然而，由于一般方程理论的决策问题通常不可解，论文强调了理论限制和特定理论的重要性，以确保算法的有效性和可行性。这项研究不仅提升了公式验证的效率，还推动了逻辑理论在实际问题中的应用。