Muutke küpsiste eelistusi

E-raamat: Automatische Synthese rekursiver Programme als Beweisverfahren

  • Formaat: PDF+DRM
  • Sari: Informatik-Fachberichte 302
  • Ilmumisaeg: 08-Mar-2013
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • Keel: ger
  • ISBN-13: 9783642847448
Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 45,68 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
Automatische Synthese rekursiver Programme als BeweisverfahrenSuurem pilt
  • Formaat: PDF+DRM
  • Sari: Informatik-Fachberichte 302
  • Ilmumisaeg: 08-Mar-2013
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • Keel: ger
  • ISBN-13: 9783642847448
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

In diesem Buch wird ein Verfahren vorgestellt, mit demInduktionsbeweise vonExistenzaussagen automatisch gef}hrtwerden k|nnen. Es ist ein deduktivesProgrammsyntheseverfahren, das ausgehend vonExistenzaussagen, die als formale Programmspezifikationenaufgefa~t werden, rekursive Programme erzeugt. Kann einsolches Programm korrekt erstellt werden, so beschreibt derSyntheseproze~ gleichzeitig einen Induktionsbeweis derentsprechenden Existenzaussage.Auf der Basis dieses Verfahrens wurde ein automatischesProgrammsynthesesystem entwickelt und implementiert. Esverwendet spezielle Transformationsregeln sowie Strategienund Heuristiken, die die Beweissuche steuern. Sie werdenanhand vieler Beispiele ausf}hrlich diskutiert.Obwohl die hier beschriebene Methode in erster Linie zurAutomatisierung von Existenzbeweisen entwickelt worden ist,und der Aspekt der automatischen Softwareentwicklung eher imHintergrund steht, motivieren zahlreiche Beispiele dazu, dasVerfahren auch f}r diesen Zweck einzusetzen.
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.
Lisainfo e-raamatute kohta Lisainfo e-raamatute kohta
Püsilink: https://www.kriso.ee/db/97836428474482e.html
Märksõnad: