ABSTRACT
We have several goals in this chapter. First, we shall investigate clausal logic and its satisfiability problem. As a consequence of the permutation lemma, we will see how special clauses, called constraints, relate to satisfiability. We also investigate unsatisfiability and its strong version, minimal unsatisfiability. The next goal of this chapter is to introduce the so-called resolution rule of proof, and then discuss the issue of the completeness of the resolution. The issue that interests us is what happens when we use the resolution rule. We will establish two basic completeness results for reasoning with clauses. Those are Theorems 7.2 (completeness theorem for resolution) and 7.8 (completeness of resolution refutation). Then we will discuss the scheme where a given CNF formula F is a knowledge base and clauses are queries. Here the idea is that the knowledge base F answers “yes” to query C if and only if F |= C. Of course, this is an obvious generalization of the propositional representation of relational databases.
