A Generalization of Stålmarck's Method
A Generalization of Stålmarck's Method
复制标题
斯托马克方法的推广
DOI：
10.1007/978-3-642-33125-1_23
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
T. Reps
中科院分区：
文献类型：
--
作者：
Aditya V. Thakur;T. Reps
本文介绍了Stalmarck的有效性检查方法的方法，并根据抽象解释领域的概念来解释每个关键组成部分。然后，我们使用这些见解为命题逻辑有效性检查算法提供了一个框架，该算法通过抽象域和该域上的操作参数化。 Stalmarck的方法是框架的一种实例化。其他实例化导致命题逻辑的新决策程序。
This paper gives an account of Stalmarck's method for validity checking of propositional-logic formulas, and explains each of the key components in terms of concepts from the field of abstract interpretation. We then use these insights to present a framework for propositional-logic validity-checking algorithms that is parametrized by an abstract domain and operations on that domain. Stalmarck's method is one instantiation of the framework; other instantiations lead to new decision procedures for propositional logic.