假设-保证推理和数组逻辑在形式化验证中的应用

2011年3月29日下午，应北京大学哲学系“逻辑、语言与认知研究中心”的邀请，来自清华大学软件学院的贺飞老师在北京大学三教101室，作了主题为“假设-保证推理和数组逻辑在形式化验证中的应用”的学术讲座。
贺飞老师首先介绍了形式化验证的基本思想。形式化验证方法主要有两种途径：定理证明和模型检测。这两种途径各有优缺点，但完全自动化、对用户的低要求等优点，使得模型检测比定理证明更具应用性。然后，贺飞老师主要介绍了模型检测技术的基本思想、基本流程、实施系统、主要限制和应用案例。
随后，贺飞老师介绍了他和他的同事们最近在模型检测方面的两项与逻辑密切相关的研究成果：
1，基于BDD（二项决策图）的通过隐式学习的假设-保证推理。
由于传统的组合式推理不适应符号化的模型检测，贺老师及其同事们提出了一种纯粹的基于BDD的假设-保证推理技术，从而提高了符号化的模型检测的检测能力。这种新的技术采取了一种BDD学习算法来生成BDD的背景假设。比较假设-保证推理与符号化的模型检测，结果显示这种新的技术推出的东西总是比在我们的实验中的背景更小的背景假设。
2，有界元素的数列逻辑（理论）。贺老师及其同事们构造了一个有界元素的一阶数列逻辑，它是一阶逻辑的一个片断。贺老师详细介绍了这个数列逻辑的语法和语义，从中可见这个逻辑在某些方面具有比较强的表达力。通过把它归约到带一个后继的弱二阶逻辑（WS1S），可以证明这种数列逻辑是可判定的。另外，可以证明这种有界数列逻辑的两种非常的自然的扩充是不可判定的。由此可见，在一阶逻辑的片断上，可判定性问题是极其微妙的。

 （王淑庆）