Suppose we have a set of clauses $\Gamma$ that are disjunctions, so that the whole set can be viewed to represent a Boolean expression in CNF form. Then we can say $\Gamma$ entails the clause $C$ iff the set $\Gamma \cup \neg C$ is unsatisfiable. (Note that $\neg C$ is a set of unit clauses.)
For any such clause $C$, we can say that it is trivially entailed by $\Gamma$ if it meets one of the following conditions:
- Subsumption: There is some clause $A \in \Gamma$ and some arbitrary disjunction $B$ such that $C = A \lor B$
- Tautology: $C$ contains both a literal and its negation, and is true in every model
Otherwise, we say that $C$ is nontrivially entailed by $\Gamma$.
One procedure that can produce nontrivial clauses is resolution, where we take two clauses sharing exactly one literal that differs in sign between them, and generate the clause that is the disjunction of all other literals in the two clauses. For example, $(a \lor b \lor c)$ and $(\neg c \lor d \lor e)$ resolve to $(a \lor b \lor d \lor e)$.
My question: Can repeated use of the resolution operator produce every non-trivially entailed clause from $\Gamma$?
In other words, do there exist non-trivially entailed clauses that we cannot obtain by repeated use of resolution on $\Gamma$ and intermediate resolvents?
Formally speaking, this is equivalent to asking if the resolution operation, coupled with operations for subsumption and tautology, leads to a strongly complete formal system. This is a much stronger criterion than "refutation completeness," which resolution is known to have.