Property of CST orollar or every sentence a and set of sentences S of L, either o the CsT from s with root Fa is a tableau proof of a from o there is a noncontradictory branch through the complete systematic tableau that yields a structure in that a is false and every element of s is trueProperty of CST Corollary For every sentence α and set of sentences S of L, either 1 the CST from S with root Fα is a tableau proof of α from S. or 2 there is a noncontradictory branch through the complete systematic tableau that yields a structure in that α is false and every element of S is true. Yi Li (Fudan University) Discrete Mathematics June 12, 2012 9 / 1