be big and it means there many nodes to handle. The we just run into a problem, how can you guarantee that every entry in generated tableau are all reduced, which means the tableau is really finishe As a tableau is at most a binary-branching tree and also be a partial ordered set. However, if we can make it order we can reduce node by node without omitting. Then we just assure a lexical graphical order, which is defined level by level and left to right on a given tableau. We just call this approach Complete Systematic Tableaux(CST)as the following Definition 4(Complete systematic tableaux. Let r be a signed proposition. We define th complete systematic tableau(Cst)with root entry R by induction 1. Let To be the unique atomic tableau with R at its root 2. 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 3. Let Tm+1 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. This method is tedious for us when the size of a proposition is small. However, it is proper for a program to reduce a given proposition with sign mechanically. CST can guarantee that no unreduced nodes are left for every entry is ordered with a number and CSt just reduce them one by one according to that order. We can check the procedure in detail. The entries are examined level by level and from left to right in the same level. Suppose CSt is processing the entries on level n. The atomic tableau corresponding to the current unreduced entry must be adjoined to the entries on the level no less than n However, there are still some issue should be taken into consideration if we really think algorith- mically. What's the time complexity for a node to be reduced and be adjoined in every noncontra dictory path which pass that node? 4 Properties of CSt There are some good properties of CSt, which will be introduced in the next class Theorem 5. Every CsT is finished Proof. Reduce the E level rel and from left to right until that there is no E unreduced for any fixed level. Every entry has a number. Given an unreduced entry En, say n. If th e current processing entry is m. After finite step, actually n-m steps, it will be reduced Theorem 6. If T= UTn is a contradictory tableau, then for some m, Tm is a finite contradictory tableau. Thus, in particular, if a CsT is a proof, it is a fimite tableau.be big and it means there many nodes to handle. The we just run into a problem, how can you guarantee that every entry in generated tableau are all reduced, which means the tableau is really finished. As a tableau is at most a binary-branching tree and also be a partial ordered set. However, if we can make it order we can reduce node by node without omitting. Then we just assure a lexical graphical order, which is defined level by level and left to right on a given tableau. We just call this approach Complete Systematic Tableaux (CST) as the following. Definition 4 (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. This method is tedious for us when the size of a proposition is small. However, it is proper for a program to reduce a given proposition with sign mechanically. CST can guarantee that no unreduced nodes are left for every entry is ordered with a number and CST just reduce them one by one according to that order. We can check the procedure in detail. The entries are examined level by level and from left to right in the same level. Suppose CST is processing the entries on level n. The atomic tableau corresponding to the current unreduced entry must be adjoined to the entries on the level no less than n. However, there are still some issue should be taken into consideration if we really think algorith￾mically. What’s the time complexity for a node to be reduced and be adjoined in every noncontra￾dictory path which pass that node? 4 Properties of CST There are some good properties of CST, which will be introduced in the next class. Theorem 5. Every CST is finished. Proof. Reduce the E level by level and from left to right until that there is no E unreduced for any fixed level. Every entry has a number. Given an unreduced entry En, say n. If the current processing entry is m. After finite step, actually n − m steps, it will be reduced. Theorem 6. If τ = ∪τn is a contradictory tableau, then for some m, τm is a finite contradictory tableau. Thus, in particular, if a CST is a proof, it is a finite tableau. 3