F(a∧B) T(a∧B) TA T a F B F(avB T(-a) T(avB) Fa Fa T B F B F(a→B) T(a分B) F T(a→B) Ta Fa t a fa FB TB FBFB Figure 1: Atomic tableaux of propositional logic 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 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 3. T is finished if every path through T is finished 4. T is contradictory if every path through T is contradictory Based on these terms, we can define what is a proof in a way with tableaux. Actually, we just prove a proposition valid by contradiction, which means we just negate its every contrary side. Definition 3. 1. A tableau proof of a proposition a is a contradictory tableau with root entry a. A proposition is tableau provable, written F a, if it has a tableau proof. 2. A tableau refutation for a proposition a is a contradictory tableau starting ith Ta. A propo sition is tableau refutable if it has a tableau refutation Of course, proof and refutation are dual to each other. Consider the following question, is refutation necessary in our proof system? 3 Complete systematic tableaux As we already know, there are many possible ways to expand the tableaux, which we mean which entry is chosen and be reduced. If the proposition is complicated enough, the parsing tree wouldT A F A T (α ∧ β) F α T β F (α ∧ β) T α F β T (¬α) F α F (¬α) T α F (α ∨ β) F α F β T (α ∨ β) T α T β T (α → β) F α T β F (α → β) T α F β T (α ↔ β) T α F α T β F β F (α ↔ β) T α F α F β T β Figure 1: Atomic tableaux of propositional logic 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. Based on these terms, we can define what is a proof in a way with tableaux. Actually, we just prove a proposition valid by contradiction, which means we just negate its every contrary side. Definition 3. 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 propo￾sition is tableau refutable if it has a tableau refutation. Of course, proof and refutation are dual to each other. Consider the following question, is refutation necessary in our proof system? 3 Complete systematic tableaux As we already know, there are many possible ways to expand the tableaux, which we mean which entry is chosen and be reduced. If the proposition is complicated enough, the parsing tree would 2