This paper gives an account of Stålmarck'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. Stålmarck's method is one instantiation of the framework; other instantiations lead to new decision procedures for propositional logic.

(Click here to access the paper: PDF.)