Stаlmark算法及其实现

摘要：

对于复杂的不可满足公式的反驳证明，Stàlmarck 算法是一个实用算法。本文利用三元组形式给出了 Stàlmarck 算法的一套推理规则及相应的 Stàlmarck 算法，并在 C 语言环境下实现了该算法。最后，我们用四元组形式给出了一套适用于不同联结词的推理规则。

关键词： 不可满足公式 Stàlmarck 算法 复杂性

作者: 董改芳 刘长云 许道云

作者单位: 贵州大学计算机科学系， 贵阳550025

会议类型: 国内会议

会议名称: 2005中国计算机大会

会议地点: 武汉

会议语种:中文

在线出版日期: 2005-10-13（万方平台首次上网日期，不代表论文的发表时间）