Finding whether a propositional formula is a tautology or not can easily be solved for the formulas having a few variables by evaluating them for each possible interpretation. However, as the number of variables increases, the number of interpretation increases exponentially and the time to solve the problem becomes unfeasible.
In this study, a statement propositional formula is first converted to a graph and then the problem is solved on that graph. In the second section, the original formula is reduced to other propositional formulas which have less variables but the same truth value. Then we try to do this reduction by other means and the concept of AND links are introduced. At last, the two dimensional forms of the propositional formulas are got. The third section shows that two dimensional formulas are equal to their statement correspondences as well as some definitions and new notations. The sections 4,5 and 6 are dedicated to investigate the properties of two dimensional formulas and find out the characteristics that differentiate a tautology from the others. These sections include most of the definitions, new notations, theorems, proofs and probably the most difficult parts to understand and follow. So I will try to summarize these sections.
The following assertions are assumed in these sections.
1. The value of a (two dimensional) formula is equal to the disjunction of the values of its elementary products.
2. The value of an elementary product is equal to the conjunction of the values of its paths.
3. The value of a path terminating with a literal or variable is equal to the value of that literal or variable.
4. The value of a unidirectional infinite path is 0.
5. If A is not a unidirectional path then the the value of the path AAA... is 1 where A is repeated infinitely.
Based on these assumpttions, the following assertions are proved.
6. The value of any returning (not unidirectional) path is 1.
7. If all the e-products in a formula have a unidirectional infinite path or a path terminating with 0(zero), then the formula is invalid. Otherwise it is valid.
To prove last assertion, it is assumed that a two dimensional formula is equal to its statement counterpart. Let SF_0 be a statement formula and TDF_0 be a two dimensional formula derived from SF_0. In the third section, it is shown that V(TDF_0)=V(SF_0) where V(TDF_0) and V(SF_0) are the values of TDF_0 and SF_0 respectively. Now reduce SF_0 to SF_1 and TDF_0 to TDF_1. The purpose is to prove that V(TDF_1)=V(SF_1) under the given assumptions. In fact, it is shown that if V(TDF_n)=V(SF_n) then V(TDF_(n+1)) = V(SF_(n+1)). Thus the reduction of two dimensional formulas is verified. Also the 6th assertion is also proved. After all the reductions, a two dimensional formula losses all of its variables and as a result of the assumptions used for verification, the 7th assertion is found to be true. After all of these, an algorithm is developed to find whether all the e-products in the given formula have a unidirectional infinite path or a unidirectional path terminating with 0(zero) in the last section. So to understand the algorithm, one does not need to investigate or understand the proofs but only need to know the assertions given.
Finding whether a statement formula is a tautology or not requires the following steps in this method.
1. Convert a statement formula to its two dimensional correspondence
2. Reduce the two dimensional formula for all of its variables
3. Apply the algorithm given in the last section to the two dimensional formula thus obtained.
Since the reduction preserves the tautological value of the original formula, if a totally reduced formula is found to be valid, then the original formula is a tautology, otherwise it is not. All of these steps require polynomial time, so the overall method takes polynomial time.