Derivation (Propositional Resolution)

propositional-logic resolution proof-theory

Definition

Derivation (Propositional Resolution)

In the propositional resolution calculus, a derivation from a set of clauses $KB$ is a sequence of clauses that starts with the input clauses and then adds clauses obtained by allowed inference steps.

If

$$KB=\{C_1,\dots ,C_k\},$$

then a derivation from $KB$ has the form

$$C_1,\dots ,C_k,C_{k+1},\dots ,C_n,\dots$$

where $C_1,\dots ,C_k$ are the input clauses, and every derived clause $C_n$ with $n\ge k+1$ is either:

• a resolvent of earlier clauses $C_i$ and $C_j$, for some $1\le i,j<n$; or
• a factor of an earlier clause $C_i$, using the factoring inference rule, for some $1\le i<n$.

A derivation is a refutation when one of its derived clauses is the empty clause $\square$.