复旦大学：《离散数学》习题课讲义（李弋）07 Tableau proof system

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

Tableau 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 9, 2013 6 / 14

Tableau 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 e 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 9, 2013 7 / 14

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 9, 2013 8 / 14

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+i be the tableau gotten by adjoining the unique atomic tableau with root e to the end of every noncontradictory path of 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 9, 2013 9 / 14

Properties of CsT Theorem 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 9, 2013 10 / 14