What you always wanted to know about clause graph resolution

1. Andrews, P.B.: Resolution with Merging, JACM, Vol. 15, No. 3 (1968), 367–381

   Article  Google Scholar 

2. Andrews, P.B.: Refutations by Matings, IEEE Trans. Comp., Vol. C-25, No. 8 (1976), 801–807

   Google Scholar 

3. Andrews, P.B.: Theorem Proving via General Matings, JACM, Vol. 28, No. 2 (1981), 193–214

   Article  Google Scholar 

4. Antoniou, G., Ohlbach, H. J.: Terminator, Proc. 8th IJCAI, Karlsruhe (1983), 916–919

   Google Scholar 

5. Bruynooghe, M.: The Inheritance of Links in a Connection Graph, Report CW2. Applied Mathematics and Programming Division, Katholieke Universiteit Leuven (1975)

   Google Scholar 

6. Brown, F.: Notes on Chains and Connection Graphs, Personal Notes. Dept. of Computation and Logic, University of Edinburgh (1976)

   Google Scholar 

7. Bibel, W.: A Strong Completeness Result for the Connection Graph Proof Procedure, Bericht ATP-3-IV-80, Institut für Informatik, Technische Universität, München (1980)

   Google Scholar 

8. Bibel, W.: On the Completeness of Connection Graph Resolution, Proc. GWAI-81, Springer Informatik Fachberichte, Vol.47, (edited by Jörg H. Siekmann), Springer, Heidelberg (1981), 246–247

   Google Scholar 

9. Bibel, W.: On Matrices with Connections, JACM, Vol. 28, No. 4 (1981), 633–645

   Article  Google Scholar 

10. Bibel, W.: A Comparative Study of Several Proof Procedures, Artificial Intelligence, Vol. 18, No. 3 (1982), 269–293

    Article  Google Scholar 

11. Bibel, W.: Automated Theorem Proving, Vieweg, Wiesbaden (1982)

    Google Scholar 

12. Chang, C.-L., Lee, R. C.-T.: Symbolic Logic and Mechanical Theorem Proving, Computer Science and Applied Mathematics Series (Editor Werner Rheinboldt), Academic Press, New York (1973)

    Google Scholar 

13. Chang, C.-L., Slagle, J. R.: Using Rewriting Rules for Connection Graphs to Prove Theorems. Artificial Intelligence, Vol.12, No. 2 (1979), 159–178

    Article  Google Scholar 

14. Eisinger, N.: Completeness, Confluence, and Related Properties of Clause Graph Resolution, Dissertation, Fachbereich Informatik, Universität Kaiserslautern (to appear 1986)

    Google Scholar 

15. Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting, JACM, Vol. 27, No. 4 (1980), 797–821

    Article  Google Scholar 

16. Kowalski, R.: Search Strategies for Theorem-Proving, Machine Intelligence (B. Meltzer and D. Michie, eds.), Vol. 5, Edinburgh University Press, Edinburgh (1970), 181–201

    Google Scholar 

17. Kowalski, R.: A Proof Procedure Using Connection Graphs. JACM, Vol. 22, No. 4 (1975), 572–595

    Article  Google Scholar 

18. Kowalski, R.: Logic for Problem Solving, Artificial Intelligence Series (Nils J. Nilsson, Editor), Vol. 7, North-Holland, New York (1979)

    Google Scholar 

19. Kowalski, R., Kuehner, D.: Linear Resolution with Selection Function, Artificial Intelligence, Vol. 2, No. 3–4 (1971), 227–260

    Article  Google Scholar 

20. Loveland, D.: Automated Theorem Proving: A Logical Basis, Fundamental Studies in Computer Science, Vol. 6, North-Holland, New York (1978)

    Google Scholar 

21. Nilsson, N.: Principles of Artificial Intelligence, Tioga, Palo Alto, CA (1980)

    Google Scholar 

22. Noll, H.: A Note on Resolution: How to Get Rid of Factoring without Losing Completeness, Proc. 5th CADE, Springer Lecture Notes in Computer Science, Vol. 87 (edited by W. Bibel and R. Kowalski), Springer, Heidelberg (1980), 250–263

    Google Scholar 

23. Shostak, R. E.: Refutation Graphs, Artificial Intelligence, Vol. 7, No. 1 (1976), 51–64

    Article  Google Scholar 

24. Shostak, R. E.: A Graph-Theoretic View of Resolution Theorem-Proving, Report SRI International, Menlo Park, CA (1979)

    Google Scholar 

25. Smolka, G.: Einige Ergebnisse zur Vollständigkeit der Beweisprozedur von Kowalski, Diplomarbeit, Fakultät Informatik, Universität Karlsruhe (1982)

    Google Scholar 

26. Smolka, G.: Completeness of the Connection Graph Proof Procedure for Unit Refutable Clause Sets, Proc. GWAI-82, Springer Informatik Fachberichte, Vol. 58 (1982), 191–204

    Google Scholar 

27. Sickel, S.: A Search Technique for Clause Interconnectivity Graphs, IEEE Trans. Comp., Vol. C-25, No. 8 (1976), 823–835

    Google Scholar 

28. Siekmann, J., Stephan, W.: Completeness and Soundness of the Connection Graph Proof Procedure, Bericht 7/76, Fakultät Informatik, Universität Karlsruhe (1976)

    Google Scholar 

29. Siekmann, J., Stephan, W.: Completeness and Consistency of the Connection Graph Proof Procedure, Interner Bericht Institut I, Fakultät Informatik, Universität Karlsruhe (1980)

    Google Scholar 

30. Wrightson, G.: An Approach to the Completeness of the Connection Graph Proof Procedure, Personal Notes, Dept. of Comp. Sc., Victoria University of Wellington, NZ (1984)

    Google Scholar 

31. Wilson, G. A., Minker, J.: Resolution, Refinements and Search Strategies: A Comparative Study, IEEE Trans. Comp., Vol. C-25, No. 8 (1976), 782–801

    Google Scholar 

32. Wos, L., Overbeek, R., Lusk, E., Boyle, J.: Automated Reasoning — Introduction and Applications, Prentice-Hall, Englewood Cliffs, NJ (1984)

    Google Scholar 

33. Wos, L., Carson, D. F., Robinson, G. A.: The Unit Preference Strategy in Theorem Proving, Proc. AFIPS-26, Spartan Books, Washington, D.C. (1964), 615–621

    Google Scholar 

34. Wos, L., Robinson, G. A., Carson, D. F.: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, JACM, Vol. 12, No. 4 (1965), 536–541

    Article  Google Scholar 

35. Yates, R. A., Raphael, B., Hart, T. P.: Resolution Graphs, Artificial Intelligence, Vol. 1, No. 3–4 (1970), 257–289

    Article  Google Scholar 

Download references