In any case, we will mostly play it by the ear so any ideas and suggestions as to what we should do this quarter are very welcome.
More specific sources will be added here as we are making progress.
First week: Our informal introduction and overview (proof systems and complexity measures) largely follows [5]. Extended Frege is p-equivalent to Substitution Frege: [1, Ch. 2.4]. CDCL vs. resolution proofs: [6]. Algebraic and semi-algebraic proofs: [7]. Line complexity, depth (called in [1] "the number of steps" and "height", respectively) and numerous relations between them in F and EF: [1, Ch. 2.5]. Space complexity: [1, Ch. 5.5], see also the original paper [8] for more general framework.
Second week (short): Introduction cntd. (notable tautologies): [5, Ch. 3 and throughout the text]. On separating F from EF: [9]. The tautologies $\neg Circuit_t{f_n}$ were explicitly introduced in [10] and extensively discussed in [11]. Basic first-order logic can be learned from any textbook in logic; [12] is my favorite. Bounded Arithmetic: [13], more modern material on the subject can be found in [1, Ch. 9].
Third week: Bounded Arithmetic cntd. Main theorem of Bounded Arithmetic (with a very rough sketch of the proof): [13, Theorems 3.1, 5.1]. The correspondence between logical theories and propositional proof systems (general framework): [1, Sct. 8.6]. The two concrete translations we mentioned are extensively dealt with in [1, Ch. 10] and [1, Ch.8], respectively. Width-size relation for resolution: [1, Sct. 5.4] or Lecture notes, Section 2. For the width lower bounds for Tseitin tautologies see the original paper [14]; [1, Ch. 13.3] contains many more examples. Polynomial calculus. Lower bounds for the pigeonhole principle (``pigeon dance'', without proof): [1, Theorem 16.2.1]. Lower bounds via the binomial method when $char(k)\neq 2$: [15] or Lecture notes, Section 7.1.2.
Fourth week: Binomial lower bounds cntd. General (non-binomial) lower bounds: [16]. For the general discussion of efficient provability of circuit lower bounds and pseudo-random generators see [11, Sec. 1] or [1, Ch. 19.4, 19.5]. Lower bounds for resolution: see [17, 18] and the literature cited therein. Lower bounds for $Res(k)$: [11]. Exponential lower bound for PHP in bounded-depth Frege: our exposition rather closely follows [1, Ch. 15].
Sixth week: Feasible interpolation cntd. Feasible interpolation for Lovasz-Schrijver: [1, Ch. 18.4] or [lecture notes, sct. A.2]. Monotone feasible interpolation, clique-coloring tautology and unconditional lower bounds for CP: [1, Ch. 18.1] or [3, Sct. 19.4.1]. Extended Frege does not admit feasible interpolation if RSA is secure: [1, Thm. 18.7.2]. Automatizability and its relation to feasible interpolation: [1, Ch. 17.3]. Our (quite brief) introduction to CDCL algorithms is based on [23]. Resolution is not automatizable unless P=NP: [24, 25]. Space complexity was introduced in [26, 27], see also [1, Ch. 5.5].
Seventh week: Space complexity cntd. Clause space vs. tree-like resolution size: [26]. Clause space vs. width: [28, 29]. Variable space vs. depth: [30]. Total space vs. width: [31]. Regularized space measures were introduced in [32] and further studied in [33]; the latter paper also contains a cumulative figure depicting what is known. Super-crtitical trade-offs between width and tree-like resolution size: [34]. Weak (sub-quadtratic) supercritical trade-offs: [32, Sct. 6] (variable space vs. length) and [35] (width vs. clause space). The lifting technique, in its modern form, was (arguably!) introduced in [36]. Lifting width lower bounds: [37].
Eighth week: Lifting width lower bounds: cntd. Lower bounds for the Binary Value Principle: Res(lin) [38] and Extended Polynomial Calculus [39]. Stabbing Planes and Tseitin tautologies: [40-42].
Nineth week: Project (Shapiro, after [24]): non-automatizability of resolution. Small Clique Problem: [43-45].