The complexity of automated reasoning
Andre N. Vellino · 1990
This thesis explores the relative complexity of proofs produced by the automatic theorem proving procedures of analytic tableaux, linear resolution, the connection method, tree resolution and the Davis-Putnam procedure. It is shown that tree resolution simulates the improved tableau procedure and that SL-resolution and the connection method are equivalent to restrictions of the improved tableau method. The theorem by Tseitin that the Davis-Putnam Procedure cannot be simulated by tree resolution is given an explicit and simplified proof. The hard examples for tree resolution are contradictions constructed from simple Tseitin graphs. iii Acknowledgements I would like to thank Steven Thomason, Marvin Belzer, David Goodman and William Older for their comments on early drafts of my thesis. I am very grateful to John Bell, James Brown, Hector Levesque, and John Slater for serving on my committee and also to William Seager for his equally interesting comments and his continual encouragemen...