Semantic trees revisited: Some new completeness results

1. Baaz, M., Fermüller, C.G.: Resolution-based Theorem Proving for Many-valued Logics. J. Symbolic Computation 11 (1995) 353–391

   Article  Google Scholar 

2. Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York and London, 1973

   Google Scholar 

3. Eisinger, N., Ohlbach, H.-J., Präcklein, A.: Reduction Rules for Resolution-Based Systems. J. Artificial Intelligence 50 (1991) 141–181

   Article  Google Scholar 

4. Fermüller, C.G.: Resolution Variant Deciding Some Classes of Clause Sets. In: Computer Science Logic (CSL'90), Heidelberg, Germany, eds. E. Börger et al., Springer Verlag, LNCS 533 (1991) 128–144

   Google Scholar 

5. Fermüller, C.G.: A Simple Resolution Based Decision Procedure for the Maslov Class. In: Developments in Theoretical Computer Science, Proceedings of the 7th IMYCS, Smolenice 1992, Gordon & Breach, 1994, 197–204

   Google Scholar 

6. Fermüller, C.G., Leitsch, A., Tammet, T., Zamov, N.: Resolution Methods for the Decision Problem. Springer Verlag, LNAI 679 (1993)

   Google Scholar 

7. Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theorie of NP-completenes. W.H. Freeman, San Francisco, 1979

   Google Scholar 

8. Gottlob, G., Fermüller, C.G.: Removing Redundancy from a Clause. J. Artificial Intelligence 61 (1993) 263–289

   Article  Google Scholar 

9. Hsiang, J., Rusinowitch, M.: Proving Refutational Completeness of TheoremProving Strategies: The Transfinite Semantic Tree Method. J. Assoc. of Comp. Mach. 38 (1991) 559–587

   Google Scholar 

10. Joyner, W.H.: Resolution Strategies as Decision Procedures. J. Assoc. of Comp. Mach. 23 (1976) 398–417

    Google Scholar 

11. Kowalski R., Hayes, P.J.: Semantic Trees in Automated Theorem Proving. In: Machine Intelligence 4 (1969), eds. B. Meltzer and D. Michie, Edinburgh University Press, 87–101

    Google Scholar 

12. Leitsch, A.: On Different Concepts of Resolution. Zeitschr. f. math. Logik und Grundlagen d. Math. 35 (1989) 71–77

    Google Scholar 

13. Loveland, D.: Automated Theorem Proving — A Logical Basis. North Holland, Amsterdam, New York, Oxford, 1978

    Google Scholar 

14. McCune W.: Otter 3.0 Users Guide. Argonne National Laboratory, Argonne (Ill.), 1990

    Google Scholar 

15. Noll, H.: A Note on Resolution: How to Get Rid of Factoring Without Loosing Completeness. In: 5th Conference on Automated Deduction, Springer Verlag, LNCS 87 (1980) 250–263

    Google Scholar 

16. Robinson, J.A.: A Machine Oriented Logic Based on the Resolution Principle. J. Assoc. of Comp. Mach. 12 (1965) 23–41

    Google Scholar 

17. Robinson, J.A.: The Generalized Resolution Principle. In: Machine Intelligence 3 (1968), ed. D. Michie, Edinburgh University Press, 77–93

    Google Scholar 

18. Slagle, J.R.: Automatic Theorem Proving with Renamable and Semantic Resolution. J. Assoc. of Comp. Mach. 14 (1967) 687–697

    Google Scholar 

19. Weidenbach, C.: Minimal Resolution. Max-Planck-Institut für Informatik, Technical report MPI-I-94-227, Saarbrücken, 1994

    Google Scholar 

Download references