Zusammenfassung
Die Einsicht, daß Herleitungen, also formalisierte Beweise, als Programme verwendet werden können, ist nicht neu: Erste Hinweise darauf sind bereits 1945 in einem Artikel von Kleene [3] zu finden. Die grundlegende Idee des Programmierens mit Herleitungen beruht auf der Tatsache, daß aus einer konstruktiven Herleitung D einer Existenzaussage ∃y B in effektiver Weise ein Term t extrahiert werden kann, der als „Zeuge“ die Richtigkeit dieser Existenzaussage belegt:
Um diesen Sachverhalt für die Programmierung nutzbar zu machen, ist es zweckmäßig, die Formel B in (1) als Beschreibung der Beziehung zwischen Eingabe x und Ausgabe y eines gewünschten Programmes zu interpretieren. Der Vorgang des Programmierens besteht dann darin, eine Herleitung D der Formel ∀x∃yB(x, y) zu konstruieren. Diese Herleitung kann nun als Programm für beliebige Eingabewerte e ausgewertet werden. Dazu wird D zunächst in naheliegender Weise auf eine Herleitung D e der Formel ∃y B(r, y) spezialisiert. Anschließend wird aus D e mit dem Verfahren von (1) ein Term te extrahiert, so daß auch die Formel B(e, t e ) herleitbar ist. Der Wert von t e ist dann der gesuchte Ausgabewert.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Literaturangaben
A. Colmerauer, H. Kanoui, P. Roussel, R. Pasero, Un système de communication homme-machine en français, Groupe de Recherche en Intelligence Artificielle, Université d’AixMarseille 1973
G. Gentzen, Untersuchungen über das logische Schließen, Math. Zeitschrift Nr. 39 (1934–5) 176–210, 405–431
S.C. Kleene, On the interpretation of intnitionistic number theory, Journal of Symb. Logic 10 (1945) 109–124
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schmerl, U.R. (1991). Herleitungen als Programme: Ihre Kompilation und Interpretation. In: Broy, M. (eds) Informatik und Mathematik. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-76677-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-76677-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-76678-7
Online ISBN: 978-3-642-76677-0
eBook Packages: Springer Book Archive