Discrete mathematics Yi li Software School Fudan University April 10, 2012
Discrete Mathematics Yi Li Software School Fudan University April 10, 2012 Yi Li (Fudan University) Discrete Mathematics April 10, 2012 1 / 1
Review o Truth assignment Truth valuation o Tautology o Consequence
Review Truth assignment Truth valuation Tautology Consequence Yi Li (Fudan University) Discrete Mathematics April 10, 2012 2 / 1
Or utline ● Tableau proof system
Outline Tableau proof system Yi Li (Fudan University) Discrete Mathematics April 10, 2012 3 / 1
Terminologies o signed proposition o entries of the tableau o atomic tableau
Terminologies signed proposition entries of the tableau atomic tableau Yi Li (Fudan University) Discrete Mathematics April 10, 2012 4 / 1
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 tableau
Tableau 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