ableau Definition(Tableaux) A finite tableau is a binary tree labeled with signed propositions called entries. such that O All atomic tableaux are finite tableaux O If T is a finite tableau, P a path on t, e an entry of T occurring on P and T' is obtained from by adjoining the unique atomic tableau with root entry e to r at the end of the path P, then T' is also a finite tableau If To, T1,..., Tn,... is a( finite or infinite) sequence of the finite tableaux such that, for each n >0, Tn+1 is constructed from Tn by an application of(2), then T=UTn is a tableauTableau Definition (Tableaux) A finite tableau is a binary tree, labeled with signed propositions called entries, such that: 1 All atomic tableaux are finite tableaux. 2 If τ is a finite tableau, P a path on τ , E an entry of τ occurring on P and τ 0 is obtained from τ by adjoining the unique atomic tableau with root entry E to τ at the end of the path P, then τ 0 is also a finite tableau. If τ0, τ1, . . . , τn, . . . is a (finite or infinite) sequence of the finite tableaux such that, for each n ≥ 0, τn+1 is constructed from τn by an application of (2), then τ = ∪τn is a tableau. Yi Li (Fudan University) Discrete Mathematics April 10, 2012 5 / 1