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 contradictoryTableau . 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