B.3 First-Order Logic 557
2. A is false, and therefore C
2
is true and can be eliminated, while A can be
eliminated from C
1
.
In the limiting case, in which C
1
and C
2
are unit clauses and the two literals are
complementary, the resolution principle generates the empty clause ∅.
If C is a resolvent of C
1
and C
2
, we say that C logically follows from C
1
and
C
2
. We can now define the notion of deduction based on resolution. Given a set
of clauses S,adeduction of the clause C from S is a finite sequence C
1
, ..., C
n
of clauses such that each C
i
either is a clause in S or is a resolvent of clauses
preceeding C
i
, and C
n
= C. A deduction of the empty clause ∅ from S is called
a refutation of S.
Example B.3 Let us build a deduction of p → r from p → q and q → r, i.e.,