A tutorial on Stalmarck's proof procedure for propositional logic
We explain Stalmarck's proof procedure fur classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale verification.
propositional logic (boolean logic) tautology checking (propositional theorem proving) dilemma proof system k-saturation proof depth tautological hardness proof complexity industrial applications of formal methods