Understanding the definition of a "restriction of a resolution derivation"

Question

I am reading the paper An Introduction to Lower Bounds on Resolution Proof Systems. In its subsection 2.3 the author gives an inductive definition of the restriction of a resolution refutation $\pi$. My preoccupation resides on the second line of the definition :

$C'_i=C'_{j_1} \vee C'_{j_2}$ if $C_{j_1} \vee y$ and $C_{j_2}\vee \bar{y}$ derive $C_i$ via the resolution rule for $j_1 < j_2 < i;$.

I wonder how this induction can be apply on $C'_{j_1}$ and $C'_{j_2}$ since $C_{j_1}$ and $C_{j_2}$ are not in $\pi$ but instead $C_{j_1}\vee y$ and $C_{j_2}\vee \bar{y}$.

Furthermore, in example 2.12 the author computes the restrictions $\pi[x_1=0]$ and $\pi[x_2=1]$ of the refutation $\pi$ as if they were just a restrictions of sets of clauses i.e. by using $\pi[x=a]=\{C[x=a]; C \in \pi\}$ instead of the inductive definition.

Is there anything that I'm missing?

Answer 1

For the first point, it seems that $C_{j_1} := D_{j_1} \lor y$ and $C_{j_2} := D_{j_2} \lor \bar{y}$ are meant to be the clauses in $\pi$, instead of $C_{j_1} \lor y$ and $C_{j_2} \lor \bar{y}$. This may help in understanding such a definition. Furthermore, it seems that the resolution of $C'_{j_1}$ and $C'_{j_2}$ upon $y$ is taken, rather than $C'_{j_1} \lor C'_{j_2}$ (they are equivalent). This view would explain, for example, the computation of $C_4[x=0]$: $C_1' = x_2 \lor \bar{x_3}$ and $C_2' = x_3$ are resolved upon $x_3$ to obtain $C_4' = x_2$.

For the second point: the computations are meant to produce the same output. In the paper, the final result without any computation is shown. Going through the recursive computation by pencil and paper shows how the rules are used.