index



For some reasons, I must publish the following paper although it is not finished yet. However, the algorithm given at the end is a complete one. The paper presents a polynomial time tautology checking method.

	Two Dimensional Formulas and Tautology Checking (pdf)(ps)

	Also this is an overview of the study. I hope it will clarify and will help to understand the method explained in the paper.



		Since the time this study is published, a mistake( and the only mistake found in the whole study) in the proof of the theorem 34 (page 71) has been found. Although it is a minor mistake, there are some counter examples that shows that the theorem is not true in general. This means that at the end of the algorithm, if the root arc is marked with an order less than 1, this does not guarantees that the formula is invalid. On the other hand, if the algorithm finds the root arc as 1, it is indeed valid. So the algorithm is not complete. Now, we present another and much simpler algorithm in the paper (tautfind.pdf). We will give the complete proof in a few days. The paper also contains a summary and explains some key points.

Hosted by www.Geocities.ws