Hostname: page-component-76fb5796d-x4r87 Total loading time: 0 Render date: 2024-04-25T07:04:22.929Z Has data issue: false hasContentIssue false
  • English
  • Français

Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen

Published online by Cambridge University Press:  15 January 2014

Peter Schroeder-Heister
Peter Schroeder-Heister*
Affiliation:
Wilhelm-Schickard-Institut, Universität Tübingen, Sand 13, 72076 Tübingen, GermanyE-mail: psh@informatik.uni-tuebingen.de
Get access Rights & Permissions [Opens in a new window]

Abstract

In the 1920s, Paul Hertz (1881–1940) developed certain calculi based on structural rules only and established normal form results for proofs. It is shown that he anticipated important techniques and results of general proof theory as well as of resolution theory, if the latter is regarded as a part of structural proof theory. Furthermore, it is shown that Gentzen, in his first paper of 1933, which heavily draws on Hertz, proves a normal form result which corresponds to the completeness of propositional SLD-resolution in logic programming.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 8 , Issue 2 , June 2002 , pp. 246 - 265
Copyright
Copyright © Association for Symbolic Logic 2002

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Abrusci, V. Michele [1983], Paul Hertz's logical works: Contents and relevance, Atti del Convegno Internazionaledi Storia della Logica, San Gimignano, 4–8 dicembre 1982 (Bologna), CLUEB, pp. 369–374.Google Scholar
Bernays, Paul [1969], Hertz, Paul. Biographical entry, Neue Deutsche Biographie (Berlin) (Historische Kommission bei der Bayerischen Akademie der Wissenschaften, editor), vol. 8, Duncker & Humblot, pp. 711–712.Google Scholar
Carnap, Rudolf [1929], Abriß der Logistik. Mit besonderer Berücksichtigung der Relationstheorie und ihrer Anwendungen, Springer, Wien.Google Scholar
Gentzen, Gerhard [1933], Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen, Mathematische Annalen, vol. 107, pp. 329–350, English translation in The Collected Papers of Gerhard Gentzen (M. E. Szabo, editor) Amsterdam, North Holland, 1969, pages 29–52.CrossRefGoogle Scholar
Gentzen, Gerhard [1934/1935], Untersuchungen über das logische Schließen, Mathematische Zeitschrift, vol. 39, pp. 176–210 and 405–431, English translation in The Collected Papers of Gerhard Gentzen (M. E. Szabo, editor), Amsterdam, North Holland 1969, pages 68–131.Google Scholar
Hertz, Paul [1922], Über Axiomensysteme für beliebige Satzsysteme. I. Teil. Sätze ersten Grades. (Über die Axiomensysteme von der kleinsten Satzzahl und den Begriff des idealen Elementes), Mathematische Annalen, vol. 87, pp. 246–269.CrossRefGoogle Scholar
Hertz, Paul [1923], Über Axiomensysteme für beliebige Satzsysteme. Teil II. Sätze hoÜheren Grades, Mathematische Annalen, vol. 89, pp. 76–102.CrossRefGoogle Scholar
Hertz, Paul [1928], Reichen die üblichen syllogistischen Regeln für das Schließen in der positiven Logik elementarer Satze aus?, Annalen der Philosophie und philosophischen Kritik, vol. 7, pp. 272–277.CrossRefGoogle Scholar
Hertz, Paul [1929], UÜber Axiomensysteme fuür beliebige Satzsysteme, Mathematische Annalen, vol. 101, pp. 457–514.CrossRefGoogle Scholar
Hertz, Paul [1929a], UÜber Axiomensysteme beliebiger Satzsysteme, Annalen der Philosophie und philosophischen Kritik, vol. 8, pp. 178–204.CrossRefGoogle Scholar
Hilbert, David [1923], Die logischen Grundlagen der Mathematik, Mathematische Annalen, vol. 88, pp. 151–165.CrossRefGoogle Scholar
Legris, Javier [1999], Paul Hertz's proof-theoretical conception of logical consequence, Unpublished Manuscript.Google Scholar
Leitsch, Alexander [1997], The resolution calculus, Springer, Berlin, etc.CrossRefGoogle Scholar
Lloyd, John W. [1987], Foundations of logic programming, 2nd ed., Springer, Berlin etc.CrossRefGoogle Scholar
Nienhuys-Cheng, Shan-Hwei and de Wolf, Ronald [1997], Foundations of inductive logic programming, Lecture Notes in Computer Science, vol. 1228, Springer, Berlin etc.CrossRefGoogle Scholar
Robinson, John A. [1963], A machine-oriented first-order logic. Abstract, The Journal of Symbolic Logic, vol. 28, p. 302. Full paper 1965: A machine-oriented logic based on the resolution principle, Journal of the Association for Computing Machinery, vol. 12, pp. 23–41.Google Scholar
Slaney, John [1989], Solution to a problem of Ono and Komori, Journal of Philosophical Logic, vol. 18, pp. 103–111.CrossRefGoogle Scholar