A Generalization of Staalmarck's Method

File(s):

Author(s): Reps, Thomas; Thakur, Aditya
Publisher: University of Wisconsin-Madison Department of Computer Sciences
Citation: TR1699
Date: Dec 2011
Subject(s): propositional logic; abstract interpretation; dilemma rule; validity checking
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.
Permanent link: http://digital.library.wisc.edu/1793/60979
Export: Export to RefWorks