Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen (Extended Version)

DSpace Repositorium (Manakin basiert)

Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen (Extended Version)

Schroeder-Heister, Peter
Dateien:
Thumbnail
324. KB
PDF
Zitierfähiger Link (URI): http://hdl.handle.net/10900/128465
http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-1284650
http://dx.doi.org/10.15496/publikation-69828
Dokumentart: Verschiedenartige Ressourcen, nicht textgeprägt
Erscheinungsdatum: 2002
Sprache: Englisch
Fakultät: 7 Mathematisch-Naturwissenschaftliche Fakultät
Fachbereich: Informatik
DDC-Klassifikation: 004 - Informatik
100 - Philosophie
510 - Mathematik
Schlagworte: Logik , Beweistheorie , Gentzen, Gerhard
Freie Schlagwörter: Hertz, Paul
Gentzen, Gerhard
Strukturregel
Resolutionsverfahren
Gentzen, Gerhard
logic
proof theory
structural rule
Hertz, Paul
resolution method
Lizenz: http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=de http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=en
Gedruckte Kopie bestellen: Print-on-Demand
Zur Langanzeige

Abstract:

Extended version of a paper with the same title, which appeared in the Bulletin of Symbolic Logic in 2002. Abstract of the (shorter) published version: "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."

Das Dokument erscheint in: