<p>I am reading the paper <a href="https://www.jstage.jst.go.jp/article/iis/21/4/21_2015.L.02/_pdf/-char/en" rel="nofollow noreferrer">An Introduction to Lower Bounds on Resolution Proof Systems</a>. 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 : </p>

<p>$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 &lt; j_2 &lt; i;$. </p>

<p>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}$.</p>

<p>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.</p>

<p>Is there anything that I'm missing?</p>

<cc.complexity-theory><proof-complexity>
Understanding the definition of a "restriction of a resolution derivation"
RTK
# Understanding the definition of a "restriction of a resolution derivation"

(Asked by: username_0 on 2018-08-30)

I am reading the paper [An Introduction to Lower Bounds on Resolution Proof Systems](https://www.jstage.jst.go.jp/article/iis/21/4/21_2015.L.02/_pdf/-char/en). 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?

**Tags:** cc.complexity-theory, proof-complexity


---

## 0 answers

