1. The depth of a proposition is the depth of associated formation tree 2. The support of a proposition is the set of propositional letters that occur as labels of the leaves of the associated formation tree Actually, all inductive proof could be based on the depth of a proposition. 4 Parsing There are infinitely many sequence of symbols. How to identify which is well-defined and which is not? If we want to build a proof system executed on a computer it is very important to construct first a method to check whether it is valid or not 4.1 Algorithm As a well-defined proposition can be uniquely mapped into a formation tree, which is easy to check every node well-defined or not. We can now introduce a recursive algorithm to analyze a sequence of symbols 1. If all leaf nodes are labeled with proposition letters, stop it. Otherwise select a leaf node having expressions other than letter and examine it 2. The first symbol must be(. if the second symbol is " jump to step 4. Otherwise go to step 3.(a)Scan the expression from the left until first reaching(a, where a is a nonempty expression having a balance between( and (b) The a is the first of the two constituents (c) The next symbol must be∧,v,→+,or分 (d) The remainder of the expression, B)must consist of a an expression B and (e) Extend the tree by adding a and B as left and right immediate successor respectively 4. The first two symbols are now known to be(. The remainder of the expression, B)must consist of a an expression B and). Then we extend the tree by adding B as its immediate successor. Goto step 1 In algorithm, we omit the procedure to exit for sequence which is not well-defined. Check every node, if a internal node is not well defined or terminal node is not a proposition letter, the algorithm just stops and asserts a non-well-defined sequence What's most important is that the algorithm checks the sequence recursively. It is the similar te the approach to define the formation tree of a well-defined proposition. According to Theorem 4 the parsing algorithm construct a unique tree1. The depth of a proposition is the depth of associated formation tree. 2. The support of a proposition is the set of propositional letters that occur as labels of the leaves of the associated formation tree. Actually, all inductive proof could be based on the depth of a proposition. 4 Parsing There are infinitely many sequence of symbols. How to identify which is well-defined and which is not? If we want to build a proof system executed on a computer it is very important to construct first a method to check whether it is valid or not. 4.1 Algorithm As a well-defined proposition can be uniquely mapped into a formation tree, which is easy to check every node well-defined or not. We can now introduce a recursive algorithm to analyze a sequence of symbols. 1. If all leaf nodes are labeled with proposition letters, stop it. Otherwise select a leaf node having expressions other than letter and examine it. 2. The first symbol must be (. if the second symbol is ¬, jump to step 4. Otherwise go to step 3. 3. (a) Scan the expression from the left until first reaching (α, where α is a nonempty expression having a balance between ( and ). (b) The α is the first of the two constituents. (c) The next symbol must be ∧, ∨, →, or ↔. (d) The remainder of the expression, β) must consist of a an expression β and ). (e) Extend the tree by adding α and β as left and right immediate successor respectively. 4. The first two symbols are now known to be (¬. The remainder of the expression, β) must consist of a an expression β and ). Then we extend the tree by adding β as its immediate successor. Goto step 1. In algorithm, we omit the procedure to exit for sequence which is not well-defined. Check every node, if a internal node is not well defined or terminal node is not a proposition letter, the algorithm just stops and asserts a non-well-defined sequence. What’s most important is that the algorithm checks the sequence recursively. It is the similar to the approach to define the formation tree of a well-defined proposition. According to Theorem 4, the parsing algorithm construct a unique tree. 4