论文部分内容阅读
逻辑公式的满足性问题是理论计算机科学和人工智能中的著名问题。命题逻辑公式的满足性判定方法和一阶逻辑公式有限模型构造技术在离散数学研究、电路辅助设计、软件工程和人工智能领域都有一些应用。
很多算法可以用来进行重言式验证，比如表算法、王浩算法以及二叉判定图BDD。二叉判定图BDD和它们的变体在其它应用方面做得也比较好，比如说模型检测等。
St(a)lmarck的重言式验证方法在一些应用上可以与二叉判定图BDD媲美，但是这个方法相对来说在硬件检测方面并不为人所知。Groote发现St(a)lmarck方法与基于BDD的方法和0tter证明器比较而言，在一个特定的荷兰火车站的安全保证系统验证中是非常高效的。
然而，St(a)lmarck方法是不完善的。虽然许多工业检测问题的难度是0或者1，对于难度为0的问题不需要使用二难规则就可以解决，但对于难度为1的问题就需要使用一级二难规则.而在此前的任何资料中都未曾提到关于St(a)lmarck方法中，二难规则中集合R1和R2的交集为空集的情况.然而这种情况是很有可能存在的。本文利用三元组形式给出了St(a)lmarck算法的一套推理规则及相应的St(a)lmarck算法，并就R1和R2的交集为空集的情况给出实例以及处理这种情况的办法并用程序(即不可满足公式的反驳证明系统)实现了这种方法，使得St(a)lmarck方法更加完善。
进一步，用四元组形式给出了一套适用于不同联结词的推理规则，用四元组集合表示公式，并对三元组形式表示规则的程序稍加修改，从而可以形成St(a)lmarck算法的一般规则判定系统。