Example 3. Is the sentence y(R(y, y)VP(, y))AVaR(a, r)) invalid? Solution. If a sentence op is invalid, then mop must be valid. So we can have the tableau proof in n) P(y, y))A VaR(, r)) By(R(, y)v P(y, y)) VcR(a T GR(co, co)V P(co, co)), new constant co T Var R(a, r) T R(co, co) T -R(Co, Co F R(Co, co) T VcR(a, a) R(t1,t1) T V R(T, T R(t2, t2) Figure 3: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid Obviously, no contradiction could be introduced in the right branch. For T(V)R(, a)exists, we can always generate new unreduced entries. So it is a infinite path. Then, when should we erminate reduction procedure? We observe that we are reducing the same set of entries periodically without introducing any valuable information in the non-contradictory path in previous example. With this observation we could terminate the reduction on that path. Generally, we always reduce those 3-style entries first. If a V-style entry use all constants generated by 3-style entries on that path, we could also terminate reduction on that path To prove a formula, we should transform it into a sentence by adding universal quantifier closure in front of it and then apply tableau proof of sentence Example 4. Check the statementExample 3. Is the sentence (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) invalid? Solution. If a sentence φ is invalid, then ¬φ must be valid. So we can have the tableau proof in figure 3. T (∃y(¬R(y, y) ∨ P(y, y)) ∧ ∀xR(x, x)) T ∃y(¬R(y, y) ∨ P(y, y)) T ∀xR(x, x) T (¬R(c0, c0) ∨ P(c0, c0)), new constant c0 T ∀xR(x, x) T R(c0, c0) T ¬R(c0, c0) T P(c0, c0) F R(c0, c0) ⊗ T ∀xR(x, x) T R(t1, t1) T ∀xR(x, x) T R(t2, t2) . . . Figure 3: An example of tableau proof The tableau is not contradictory. So the sentence is not invalid. Obviously, no contradiction could be introduced in the right branch. For T(∀x)R(x, x) exists, we can always generate new unreduced entries. So it is a infinite path. Then, when should we terminate reduction procedure? We observe that we are reducing the same set of entries periodically without introducing any valuable information in the non-contradictory path in previous example. With this observation, we could terminate the reduction on that path. Generally, we always reduce those ∃-style entries first. If a ∀-style entry use all constants generated by ∃-style entries on that path, we could also terminate reduction on that path. To prove a formula, we should transform it into a sentence by adding universal quantifier closure in front of it and then apply tableau proof of sentence. Example 4. Check the statement {(ψ(x) → (∃x)φ(x))} ⊢ (∃x)(ψ(x) → φ(x)) 4