Property of CST orollar For 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 4, 2013 9 / 17