Discrete mathematics Yi li Software School Fudan University April 9. 2013
. . Discrete Mathematics Yi Li Software School Fudan University April 9, 2013 Yi Li (Fudan University) Discrete Mathematics April 9, 2013 1 / 14
Re eview o Truth assignment Truth valuation o Tautology o Consequence
Review Truth assignment Truth valuation Tautology Consequence Yi Li (Fudan University) Discrete Mathematics April 9, 2013 2 / 14
Or utline Tableau proof system
Outline Tableau proof system Yi Li (Fudan University) Discrete Mathematics April 9, 2013 3 / 14
Terminologies ● signed proposition entries of the tableau o atomic tableau
Terminologies signed proposition entries of the tableau atomic tableau Yi Li (Fudan University) Discrete Mathematics April 9, 2013 4 / 14
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 τ ′ is obtained from τ by adjoining the unique atomic tableau with root entry E to τ at the end of the path P, then τ ′ 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 9, 2013 5 / 14