Boolean formulas

Boolean formulas can be used to express constraint satisfaction problems in general, among other things. The manner in which we solve boolean formulas is defined by resolution. Assuming that a given boolean formula is effectively expressed in conjunctive normal formula we can apply resolution to any two clauses in the boolean formula which have complementary literals, which will get us a new clause which contains all literals that do not have complements. Well applying the resolution rule, if we get a clause that is simpler then some larger clause that contains it, we can eliminate the larger clauses. This is one way we can use deduction to solve logic problems.