Automatisierung von Terminierungsbeweisen

Paperback Duits 1991 1991e druk 9783528047719
Verwachte levertijd ongeveer 9 werkdagen

Samenvatting

Das Fuhren von Terminierungsbeweisen flir rekursiv definierte Algorithmen erfordert eine gewisse Kreativitiit des (menschlichen oder automatischen) Bewei­ sers, die sich im Erfinden einer Hypothese manifestiert, deren Giiltigkeit hinrei­ chend flir die Terminierung eines Algorithmus ist. In dieser Arbeit wird ein Ver­ fahren vorgestellt, mit dem diese KreativiUit durch ein Computerprogramm nachgebildet werden soIl. Mit diesem Verfahren konnen Terminierungsbeweise in vielen Hillen vollautomatisch, d.h. ohne jegliche menschliche Unterstutzung, gefiihrt werden. Es wird gezeigt, - wie flir einen Algorithmus eine Terminierungshypothese automatisch synthetisiert werden kann, - welches Wissen uber Algorithmen dazu erforderlich ist, - wie dieses Wissen reprasentiert wird, und - wie dieses Wissen durch eine Maschine selbst berechnet werden kann. Das hier beschriebene Verfahren lOst die gestellte Aufgabe fUr eine relevante Klasse von Algorithmen, wie etwa klassische Sortieralgorithmen und Algorith­ men flir grundlegende arithmetische Operationen, die in einer rein funktionalen Programmiersprache gegeben sind. Die hier vorliegende Arbeit, die in den Jahren 1984 -1988 entstand, wurde zum Teil durch den Sonderforschungsbereich 314 "Kunstliche Intelligenz und Wissensbasierte Systeme" der Deutschen Forschungsgemeinschaft gefOrdert und von der Fakultat flir Informatik der Universitat Karlsruhe als Habilitations­ schrift angenommen. Ich danke Prof. Dr. P. Deussen flir die Arbeitsmoglichkei­ ten und Unterstiitzung wahrend der Jahre an seinem Institut.

Specificaties

ISBN13:9783528047719
Taal:Duits
Bindwijze:paperback
Aantal pagina's:253
Druk:1991

Lezersrecensies

Wees de eerste die een lezersrecensie schrijft!

Inhoudsopgave

1 Einleitung.- 1.1 EinTerminierungsbeweis für einen Sortieralgorithmus.- 1.2 Das Termenierungsverfahren — Ein Überblick.- 1.3 Bibliographische Anmerkungen und verwandte Arbeiten.- 2 Syntaktische und semantische Begriffe.- 2.1 Syntaktische definitionen.- 2.2 semantik der sprache erster stufe.- 2.3 standardalgebren und Standardmodelle.- 2.4 Fundierte Ordnungen.- 3 Spezifikationen.- 3.1 Datenstrukturen.- 3.2 Algorithmen.- 3.3 Normalformen für Algorithmen.- 3.4 Zulässige spezifikationen und Beweisen durch Induktion.- 3.5 Zusammenfassung.- 4 Beweisen durch Abschätzen mit dem E-Kalkül.- 4.1 Die Anzahlordnung.- 4.2 Abschätzungen durch argumentbeschränkte Operationen.- 4.3 Differenzliterale für argumentbeschränkte Operationen.- 4.4 Abschätzungen durch Datenstrukturen.- 4.5 Formale Definition und Korrektheit des E-Kalküls.- 4.6 Das Differenzäquivalent.- 4.7 Ein Beweisverfahren für den E-Kalkül.- 4.8 Zusammenfassung.- 5 Erzeugung von Terminierungshypothesen.- 5.1 Terminierungshypothesen durch Abschätzungen.- 5.2 Ein Terminierungskriterium mit Termrepräsentanten.- 5.3 Algorithmen in positiver Strukturnormalform.- 5.4 Lexikographische Terminierungsordnungen.- 5.5 Terminierungshypothesen für das ‘Sort’-Beispiel.- 5.6 Zusammenfassung.- 6 Erkennen argumentbeschränkter Operationen.- 6.1 Reflexive Selektoren.- 6.2 Argumentbeschränkte Algorithmen.- 6.3 Synthese von differenzalgorithmen.- 6.4 Zusammenfassung.- 7 Optimierung von Differenzalgorithmen.- 7.1 Bedingungssubsumption.- 7.2 Termvereinfachung.- 7.3 Rekursionselimination.- 7.4 Fallverschmelzung.- 7.5 Zusammenfassung.- 8 Algorithmenmodifikation.- 8.1 Transformation von Ergebnistermen.- 8.2 Transformation von Bedingungen.- 8.3 Die Aufgabe des Benutzers.- 8.4 Zusammenfassung.- 9 Implementierung.

Managementboek Top 100

Rubrieken

Populaire producten

    Personen

      Trefwoorden

        Automatisierung von Terminierungsbeweisen