A Generalization of Staalmarck's Method

Abstract

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