Davis-Putnam Style Rules for Deciding Property S

Abstract

Two set systems E, F on an underlying set V will be said to have Property S if there exists a subset σ of V , such that σ∩ e ≠Ø, for all e ∈ E and f ⊈σ, for all f ∈ F (see [8], [9]]). We give rules for deciding Property S, which generalizes the very successful Davis-Putnam rules for deciding satisfiability in propositional logic.