A theoretical basis for the systematic proof method

1. P.B. Andrews, Refutations by matings, IEEE Transactions on Computer C-25 (1976) 801–807.

   Google Scholar 

2. P.B. Andrews, Theorem Proving via General Matings, Journal of the ACM (to appear).

   Google Scholar 

3. W. Bibel, An approach to a systematic theorem proving procedure in first-order logic, Computing 12 (1974) 43–55.

   Google Scholar 

4. W. Bibel, Maschinelles Beweisen, Jahrbuch Überblicke Mathematik (Bibliographisches Institut, Mannheim, 1976) 115–142.

   Google Scholar 

5. W. Bibel, Tautology testing with a generalized matrix reduction method, Theoretical Computer Science 8 (1979), 31–44.

   Google Scholar 

6. W. Bibel, On matrices with connections, Bericht 79, Universität Karlsruhe (1979), submitted to JACM.

   Google Scholar 

7. W. Bibel, A comparative study of several proof procedures, Proc. AISB-80 (1980).

   Google Scholar 

8. W. Bibel, Syntax-directed, semantics-supported program synthesis, Artificial Intelligence Journal (to appear).

   Google Scholar 

9. W. Bibel and J. Schreiber, Proof search in a Gentzen-like system of first-order logic, Proc. Int. Computing Symposium (North-Holland, Amsterdam, 1975) 205–212. Also contained in: W. Bibel, Programmieren in der Sprache der Prädikatenlogik, Habilitationsarbeit (abgelehnt), Technische Universität München (1975).

   Google Scholar 

10. W.W. Bledsoe, Non-resolution theorem proving, Artificial Intelligence 9 (1977) 1–35.

    Google Scholar 

11. J. Friedrich, Ein systematischer Algorithmus zum Beweisen von Theoremen in einem Prädikatenkalkül erster Ordnung, Diplomarbeit, Techn. Univ. München (1973).

    Google Scholar 

12. G. Gentzen, Untersuchungen über das logische Schließen I, Mathemat. Zeitschrift 39, (1935) 176–210.

    Google Scholar 

13. C.A. Goad, Proofs as descriptions of programs, Proc. CADE-5, Springer (to appear).

    Google Scholar 

14. J. Herbrand, Recherches sur la Theorie de la Demonstration, Travaux de la Societe des Sciences et des Lettres de Varsovie, Classe III sciences mathematiques et physiques, 33 (1930).

    Google Scholar 

15. G. Huet, Résolution d'équations dans des languages d'ordres 1,2,...,ω, Thèse de doctorat d'état, Université Paris VII (1976).

    Google Scholar 

16. G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Rapport Laboria n^o 250, IRIA-LABORIA, Domaine de Voluceau, 78150 Le Chesnay, France (1977).

    Google Scholar 

17. R. Kowalski, Algorithm = logic + control, Comm. of the ACM 22 (1979) 424–436.

    Google Scholar 

18. Z. Manna, R. Waldinger, A deductive approach to program synthesis, Proc. IJCAI-79 (1979) 542–551.

    Google Scholar 

19. S.J. Maslow, The inverse method for establishing deducibility for logical calculi, Proc. Steklov Inst. Math. 98 (1968).

    Google Scholar 

20. D. Prawitz, An improved proof procedure, Theoria 26 (1960) 102–139.

    Google Scholar 

21. J.A. Robinson, Logic: form and function, Edinburgh University Press (1979).

    Google Scholar 

22. M. Sato, Towards a mathematical theory of program synthesis, Proc. IJCAI-79 (1979) 757–762.

    Google Scholar 

23. J. Schreiber, Vergleichende qualitative und quantitative Untersuchungen von Beweisverfahren, Bericht Nr. 7411, Technische Universität München (1974).

    Google Scholar 

24. K. Schütte, Proof theory, Springer Verlag (Berlin, 1977).

    Google Scholar 

Download references