Hugendubel.info - Die B2B Online-Buchhandlung 

Merkliste
Die Merkliste ist leer.
Bitte warten - die Druckansicht der Seite wird vorbereitet.
Der Druckdialog öffnet sich, sobald die Seite vollständig geladen wurde.
Sollte die Druckvorschau unvollständig sein, bitte schliessen und "Erneut drucken" wählen.

Automatische Synthese rekursiver Programme als Beweisverfahren

BuchKartoniert, Paperback
259 Seiten
Deutsch
Springererschienen am08.04.1992
In diesem Buch wird ein Verfahren vorgestellt, mit dem Induktionsbeweise vonExistenzaussagen automatisch gef}hrt werden k|nnen. Es ist ein deduktives Programmsyntheseverfahren, das ausgehend von Existenzaussagen, die als formale Programmspezifikationen aufgefa~t werden, rekursive Programme erzeugt. Kann ein solches Programm korrekt erstellt werden, so beschreibt der Syntheseproze~ gleichzeitig einen Induktionsbeweis der entsprechenden Existenzaussage. Auf der Basis dieses Verfahrens wurde ein automatisches Programmsynthesesystem entwickelt und implementiert. Es verwendet spezielle Transformationsregeln sowie Strategien und Heuristiken, die die Beweissuche steuern. Sie werden anhand vieler Beispiele ausf}hrlich diskutiert. Obwohl die hier beschriebene Methode in erster Linie zur Automatisierung von Existenzbeweisen entwickelt worden ist, und der Aspekt der automatischen Softwareentwicklung eher im Hintergrund steht, motivieren zahlreiche Beispiele dazu, das Verfahren auch f}r diesen Zweck einzusetzen.mehr
Verfügbare Formate
BuchKartoniert, Paperback
EUR54,99
E-BookPDF1 - PDF WatermarkE-Book
EUR42,99

Produkt

KlappentextIn diesem Buch wird ein Verfahren vorgestellt, mit dem Induktionsbeweise vonExistenzaussagen automatisch gef}hrt werden k|nnen. Es ist ein deduktives Programmsyntheseverfahren, das ausgehend von Existenzaussagen, die als formale Programmspezifikationen aufgefa~t werden, rekursive Programme erzeugt. Kann ein solches Programm korrekt erstellt werden, so beschreibt der Syntheseproze~ gleichzeitig einen Induktionsbeweis der entsprechenden Existenzaussage. Auf der Basis dieses Verfahrens wurde ein automatisches Programmsynthesesystem entwickelt und implementiert. Es verwendet spezielle Transformationsregeln sowie Strategien und Heuristiken, die die Beweissuche steuern. Sie werden anhand vieler Beispiele ausf}hrlich diskutiert. Obwohl die hier beschriebene Methode in erster Linie zur Automatisierung von Existenzbeweisen entwickelt worden ist, und der Aspekt der automatischen Softwareentwicklung eher im Hintergrund steht, motivieren zahlreiche Beispiele dazu, das Verfahren auch f}r diesen Zweck einzusetzen.
Details
ISBN/GTIN978-3-540-55300-7
ProduktartBuch
EinbandartKartoniert, Paperback
Verlag
Erscheinungsjahr1992
Erscheinungsdatum08.04.1992
ReiheInformatik-Fachberichte
Seiten259 Seiten
SpracheDeutsch
Gewicht442 g
IllustrationenVIII, 259 S.
Artikel-Nr.18222214

Inhalt/Kritik

Inhaltsverzeichnis
1. Einführung.- 2. Übersicht.- 3. Formale Grundbegriffe.- 3.1 Syntaktische Grundbegriffe.- 3.2 Semantische Grundbegriffe.- 3.3 Theoriespezifikationen.- 4. Beweis durch Synthese.- 4.1 Der Synthesekalkül.- 4.2 Korrektheit.- 5. Transformationsregeln.- 5.1 Induktionsregeln.- 5.2 Normalisierung.- 5.3 Termersetzungsregeln.- 5.4 Fallunterscheidungsregeln.- 5.5 Extraktionsregeln.- 5.6 Implikationenregel.- 5.7 Eliminationsregel.- 6. Das Syntheseverfahren als Existenzbeweismethode.- 6.1 Auswahl eines geeigneten Induktionsaxioms.- 6.2 Konstruktion eines lösenden Terms.- 6.3 Verwendung von Eigenschaften des lösenden Terms zum Beweis.- 7. Die Mechanisierung des Verfahrens.- 7.1 Die Struktur des Suchraumes.- 7.2 Die Suchstrategie.- 7.3 Die vier Phasen des Syntheseprozesses.- 7.4 Die Zulässigkeit des synthetisierten Programmes.- 8. Heuristiken.- 8.1 Auswahl der Induktionsaxiome.- 8.2 Symbolische Auswertung.- 8.3 Verwendung von Induktionshypothesen.- 8.4 Lösung von Konflikten.- 8.5 Verwendung von Bedingungen.- 8.6 Auswahl von Restformeln.- 8.7 Bewertung von Regelanwendungen.- 9. Beispiele.- 9.1 Die Vollständigkeit eines Beweisers für Aussagenlogik.- 9.2 Die Synthese einer Funktion zur Umkehrung von Listen.- 9.3 Die Synthese einer Sortierfunktion.- 9.4 Die Synthese von ganzzahligem Quotient und Rest.- 10. Schlußbemerkungen.- Literatur.- Anhang A: Sorten, Stellen und Ordnungsrelationen.- Anhang B: Verzeichnis der Symbole und Abkürzungen.mehr