دسترسی نامحدود
برای کاربرانی که ثبت نام کرده اند
برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید
در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید
برای کاربرانی که ثبت نام کرده اند
درصورت عدم همخوانی توضیحات با کتاب
از ساعت 7 صبح تا 10 شب
ویرایش: 1
نویسندگان: Susanne Biundo (auth.)
سری: Informatik-Fachberichte 302
ISBN (شابک) : 9783540553007, 9783642847448
ناشر: Springer-Verlag Berlin Heidelberg
سال نشر: 1992
تعداد صفحات: 262
زبان: German
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود)
حجم فایل: 6 مگابایت
کلمات کلیدی مربوط به کتاب سنتز خودکار برنامه های بازگشتی به عنوان روش اثبات: منطق و معانی برنامه ها
در صورت تبدیل فایل کتاب Automatische Synthese rekursiver Programme als Beweisverfahren به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.
توجه داشته باشید کتاب سنتز خودکار برنامه های بازگشتی به عنوان روش اثبات نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.
در این کتاب روشی ارائه شده است که با آن می توان به طور خودکار برهان استقرایی گزاره های وجود را بیان کرد. این یک روش ترکیب برنامه قیاسی است که برنامه های بازگشتی را با شروع از عبارات وجودی که به عنوان مشخصات برنامه رسمی درک می شوند، تولید می کند. اگر بتوان چنین برنامه ای را به درستی ایجاد کرد، فرآیند سنتز به طور همزمان یک اثبات استقرایی از عبارت وجود متناظر را توصیف می کند. بر اساس این روش، یک سیستم سنتز برنامه خودکار توسعه و پیاده سازی شد. از قوانین تبدیل ویژه و همچنین استراتژیها و اکتشافیهایی استفاده میکند که جستجوی شواهد را کنترل میکنند. آنها با استفاده از مثال های زیادی به تفصیل مورد بحث قرار می گیرند. اگرچه روشی که در اینجا توضیح داده شد در درجه اول برای خودکارسازی اثبات وجود توسعه داده شد و جنبه توسعه خودکار نرمافزار بیشتر در پسزمینه است، نمونههای متعدد انگیزه استفاده از روش را برای این منظور نیز فراهم میکنند.
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.
Front Matter....Pages N2-VIII
Einführung....Pages 1-13
Übersicht....Pages 15-17
Formale Grundbegriffe....Pages 19-41
Beweis durch Synthese....Pages 43-56
Transformationsregeln....Pages 57-90
Das Syntheseverfahren als Existenzbeweismethode....Pages 91-111
Die Mechanisierung des Verfahrens....Pages 113-145
Heuristiken....Pages 147-192
Beispiele....Pages 193-240
Schlußbemerkungen....Pages 241-243
Back Matter....Pages 245-259