Deductions from premises How to construct CST from premises Definition(Tableaux from premises) Let 2 be(possibly infinite)set of propositions. We define the finite tableaux with premises from 2 by induction: | t is a finite tableau from∑anda∈∑, then the tableau formed by putting Ta at the end of every noncontradictory path not containing it is also a finite tableau from∑Deductions from Premises How to construct CST from premises? Definition (Tableaux from premises) Let Σ be (possibly infinite) set of propositions. We define the finite tableaux with premises from Σ by induction: 2 If τ is a finite tableau from Σ and α ∈ Σ, then the tableau formed by putting Tα at the end of every noncontradictory path not containing it is also a finite tableau from Σ. Yi Li (Fudan University) Discrete Mathematics April 24, 2012 6 / 25