The practicality of generating semantic trees for proofs of unsatisfiability

References

• Bledsoe , W. W. 1971 . Splitting and reduction heuristics in automatic theorem proving . Artificial Intelligence , 2 : 57 – 78 .
   Google Scholar
• Chang , C. L. and Lee , R. C. T. 1973 . Symbolic Logic and Mechanical Theorem Proving , Academic Press .
   Google Scholar
• Chang C. L. Theorem proving by generation of pseudo-semantic trees, Div. of Comput. Res. and TechnoL, Nat. Inst, of Health Bethesda, Maryland 1971
   Google Scholar
• Hsiang , J. and Rusinowitch , M. 1991 . Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method . Journal of the Assoc, for Computing Machinery , 38 ( 3 ) : 559 – 587 .
   Web of Science ®Google Scholar
• Kowalski , R. 1970 . Search strategies for theorem-proving . Machine Intelligence , 5 : 87 – 101 .
   Google Scholar
• Kowalski , R. and Hayes , J. P. 1969 . Semantic trees in automatic theorem-proving . Machine Intelligence , 4 : 87 – 101 .
   Google Scholar
• Letz , R. , Bayerl , S. and Bibel , W. 1992 . SETHEO, a high performance theorem prover . Journal of Automated ReasoningrH , 4 : 183 – 213 .
   Google Scholar
• Loveland , D. W. 1978 . Automated Theorem Proving: A lagical Basis , Vol. 6 , North-Holland Publishing Company .
   Google Scholar
• Manna , Z. 1974 . Mathematical Theory of Computation , McGraw-Hill Computer Science Series .
   Google Scholar
• Newborn M. The Great Theorem Prover Version 2, Newborn Software 1994
   Google Scholar
• Nilsson , N. J. 1971 . Problem-Solving Methods in Artificial Intelligence , McGraw-Hill Inc .
   Google Scholar
• Norton , L. M. 1971 . Experiments with a heuristic theorem-proving for the predicate calculus with equality . Artificial Intelligence , 2 ( 3/4 ) : 261 – 284 .
   Google Scholar
• Robinson , J. 1965 . A machine oriented logic based on the resolution principle . Journal of the Assoc, for Computing Machinery , 12 ( 1 ) : 23 – 41 .
   Web of Science ®Google Scholar
• Sikloosy L. Marinov V. Heuristic search vs. exhaustive search, Proc. 2nd International Conference on Artificial Intelligence London 1971 601 607
   Google Scholar
• Slagle , J. R. and Farrell , C. D. 1971 . Experiments in automatic learning for a multipurpose heuristic program . Comm. Assoc, for Computing Machinery , 14 : 91 – 99 .
   Google Scholar
• Slagle , J. R. 1967 . Automatic theorem-proving with renamable and semantic resolution, Journal of the Assoc . for Computing Machinery , 14 ( 4 ) : 687 – 697 .
   Web of Science ®Google Scholar
• Stickel , M. E. and Stoll , R. 1963 . Set Theorey And Logic , Freeman W. H. and Company .
   Google Scholar
• Stoll R. Set Theorey And Logic A series of books inmathematics. 1963 Freeman, W. H. and Company
   Google Scholar