复旦大学：《离散数学 Discrete Mathematics》英文讲稿_07 Tableau proof system

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

ableau Example a tableau with the signed proposition F((a→B)(Vb)∧(avB)

Tableau Example A tableau with the signed proposition F(((α → β) ∨ (γ ∨ δ)) ∧ (α ∨ β)). Yi Li (Fudan University) Discrete Mathematics April 10, 2012 6 / 1

ableau Definition Let r be a tableau, p a path on t and e an entry occurring on P o E has been reduced on P if all the entries on one path through the atomic tableau with root e occur on p o P is contradictory if, for some proposition a, Ta and Fa are both entries on P. P is finished if it is contradictory or every entry on P is reduced on P O T is finished if every path through T is finished O T is contradictory if every path through T is contradictory

Tableau Definition Let τ be a tableau, P a path on τ and E an entry occurring on P. 1 E has been reduced on P if all the entries on one path through the atomic tableau with root E occur on P. 2 P is contradictory if, for some proposition α, Tα and Fα are both entries on P. P is finished if it is contradictory or every entry on P is reduced on P. 3 τ is finished if every path through τ is finished. 4 τ is contradictory if every path through τ is contradictory. Yi Li (Fudan University) Discrete Mathematics April 10, 2012 7 / 1

Proof Definition o a tableau proof of a proposition a is a contradictory tableau with root entry Fa. A proposition is tableau provable, written H a, if it has a tableau proof o a tableau refutation for a proposition a is a contradictory tableau starting with Ta. A proposition is tableau refutable if it has a tableau refutation

Proof Definition 1 A tableau proof of a proposition α is a contradictory tableau with root entry Fα. A proposition is tableau provable, written ` α, if it has a tableau proof. 2 A tableau refutation for a proposition α is a contradictory tableau starting with Tα. A proposition is tableau refutable if it has a tableau refutation. Yi Li (Fudan University) Discrete Mathematics April 10, 2012 8 / 1

Complete Systematic Tableaux Definition( Complete systematic tableaux) Let r be a signed proposition. We define the complete systematic tableau(CSt) with root entry R by induction o Let To be the unique atomic tableau with r at its root. Q Assume that Tm has been defined. let n be the smallest level of Tm and let e be the leftmost such entry of level n O Let Tm+1 be the tableau gotten by adjoining the unique atomic tableau with root e to the end of every noncontradict Tm on which E is unreduced The union of the sequence Tm is our desired complete systematic tableau

Complete Systematic Tableaux Definition (Complete systematic tableaux) Let R be a signed proposition. We define the complete systematic tableau(CST) with root entry R by induction. 1 Let τ0 be the unique atomic tableau with R at its root. 2 Assume that τm has been defined. Let n be the smallest level of τm and let E be the leftmost such entry of level n. 3 Let τm+1 be the tableau gotten by adjoining the unique atomic tableau with root E to the end of every noncontradictory path of τm on which E is unreduced. The union of the sequence τm is our desired complete systematic tableau. Yi Li (Fudan University) Discrete Mathematics April 10, 2012 9 / 1

Properties of CsT eorem Every CST is finished Reduce the E level by level and there is no E unreduced for any fixed

Properties of CST Theorem Every CST is finished. Proof. Reduce the E level by level and there is no E unreduced for any fixed level. Yi Li (Fudan University) Discrete Mathematics April 10, 2012 10 / 1