Die Mathe-Redaktion - 29.01.2020 00:50 - Registrieren/Login
Auswahl
ListenpunktHome
ListenpunktAktuell und Interessant ai
ListenpunktArtikelübersicht/-suche
ListenpunktAlle Links / Mathe-Links
ListenpunktFach- & Sachbücher
ListenpunktMitglieder / Karte / Top 15
ListenpunktRegistrieren/Login
ListenpunktArbeitsgruppen
Listenpunkt? im neuen Schwätz
ListenpunktWerde Mathe-Millionär!
ListenpunktZur Award-Gala
ListenpunktFormeleditor fedgeo
Schwarzes Brett
Aktion im Forum
Suche
Stichwortsuche in Artikeln und Links von Matheplanet
Suchen im Forum
Suchtipps

Bücher
Englische Bücher
Software
Suchbegriffe:
Mathematik bei amazon
Naturwissenschaft & Technik
In Partnerschaft mit Amazon.de
Kontakt
Mail an Matroid
[Keine Übungsaufgaben!]
Impressum

Bitte beachten Sie unsere Nutzungsbedingungen, die Distanzierung, unsere Datenschutzerklärung und
die Forumregeln.

Sie können Mitglied werden. Mitglieder können den Matheplanet-Newsletter bestellen, der etwa alle 2 Monate erscheint.

Der Newsletter Okt. 2017

Für Mitglieder
Mathematisch für Anfänger
Wer ist Online
Aktuell sind 426 Gäste und 8 Mitglieder online.

Sie können Mitglied werden:
Klick hier.

Über Matheplanet
 
Zum letzten Themenfilter: Themenfilter:
Matroids Matheplanet Forum Index
Moderiert von Bilbo
Theoretische Informatik » Berechenbarkeitstheorie » Spezifikation des Halteproblems angeben
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule Spezifikation des Halteproblems angeben
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1025
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2019-11-26


Hallo allerseits,
=====================================
In seinem Buch "Ideen der Informatik" schreibt Uwe Schöning:
Gegeben ist ein auf Korrektheit zu analysierendes Programm A und eine Spezifikation S (die genau beschreibt, was es heißt formal korrekt zu sein).
Dies ist eine Ansammlung von Formeln, die Aussagen darüber machen welche Eigenschaften die im Programm vorkommenden Variablen nach der Ausführung des Programms haben sollten unter Bezugnahme der Werte der Variablen, die  vor Ausführung des Programms A galten.
Wenn es einen solchen Verifikationsalgorithmus geben würde, könnte er das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann).
=====================================

Frage:
Wie kann man die Spezifikation des Halteproblem angeben ?
Das muß doch eine prädikatenlogische Formel sein.

mfg
cx





  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 02.12.2013
Mitteilungen: 212
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, eingetragen 2019-11-28


2019-11-26 19:16 - carlox im Themenstart schreibt:
Hallo allerseits,
=====================================
In seinem Buch "Ideen der Informatik" schreibt Uwe Schöning:
Gegeben ist ein auf Korrektheit zu analysierendes Programm A und eine Spezifikation S (die genau beschreibt, was es heißt formal korrekt zu sein).
Dies ist eine Ansammlung von Formeln, die Aussagen darüber machen welche Eigenschaften die im Programm vorkommenden Variablen nach der Ausführung des Programms haben sollten unter Bezugnahme der Werte der Variablen, die  vor Ausführung des Programms A galten.
Wenn es einen solchen Verifikationsalgorithmus geben würde, könnte er das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann).
=====================================

Frage:
Wie kann man die Spezifikation des Halteproblem angeben ?
Das muß doch eine prädikatenlogische Formel sein.

Ja, das ist eine prädikatenlogische Formel. Die kann man hier aber nicht angeben. Man braucht dazu ja einige Begriffe mittels derer man die Spezifikation formulieren kann. Allein diese Begriffe formal zu definieren und damit dann die Spezifikation als Formel aufzuschreiben ist kein einfaches Unterfangen.

Boyer und Moore haben die Unlösbarkeit des Halteproblems vor 35 Jahren mit ihrem Verifikationssystem bewiesen dl.acm.org/citation.cfm?doid=828.1882 . In dem Artikel findet man die Spezifikation - ist aber schwere Kost!  

PS1: "Prädikatenlogische Formel" heißt natürlich nicht "mittels Prädikatenlogik beweisbar". Da Programme Schleifen bzw. Rekursion enthalten braucht man Induktion.

PS2: Was ist denn mit >solchen< Verifikationsalgorithmus gemeint?




  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1025
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, vom Themenstarter, eingetragen 2019-11-29


hallo Zwerg_Allwissend,
Vielen Dank für deine Antwort.

1)
>Ja, das ist eine prädikatenlogische Formel.
>Die kann man hier aber nicht angeben
> Man braucht dazu ja einige Begriffe mittels derer man
>die Spezifikation formulieren kann.
>Allein diese Begriffe formal zu definieren und
>damit dann die Spezifikation als Formel aufzuschreiben ist
>kein einfaches Unterfangen.
>
Das denke ich auch.
Die Spezifikation besteht aus einer Vorbedingung P und einer Nachbedingung Q.
P ist eine prädikatenlogische Formel, die die im Programm A vorkommenden Werte der Variablen vor der Programmausführung betrifft und Q ist eine prädikatenlogische Formel, die die in A vorkommenden Werte der Variablen nach der Programmausführung betrifft.
In einer der in P vorkommenden Variablen (ich nenne sie e) steht dann das zu untersuchende Programm R, also (informal):
e = R
Das zu formalisieren dürfte kein Ptoblem sein: Man nimmt für R einfach die codierte Turingmaschine, die das Programm R darstellt, also eine Zahl.  

In einer der in Q vorkommenden Variablen (ich nenne sie o) steht dann eine Zeichenfolge "R hält an" oder "R hält nicht a" also:
o = "R hält an"  , wenn R anhält  
o = "R hält nicht an"  , wenn R nicht anhält  
Das Problem ist, wie man diese Verzweigung durch eine prädikatenlogische Formel darstellt.
Das dürfte schwierig sein (wie formalisiert man "R hält an" bzw "R hält nicht an"?)    
Oder sehe ich da was falsch ?

2)
>Boyer und Moore haben die Unlösbarkeit des Halteproblems vor 35 Jahren
>mit ihrem Verifikationssystem bewiesen dl.acm.org/citation.cfm?doid=828.1882 .
>In dem Artikel findet man die Spezifikation - ist aber schwere Kost!  
>
a) Habe versucht den Artikel runterzulade (obwohl ich vermutlich den nicht verstehen werde).
Das kostet Geld  oder gibt es den auch kostenlos?

b)
Bis jetzt dachte ich , daß  man unter Programmverifikation (=Verifikationssystem) versteht, dass man die Korrektheit eines konkret vorgegebenen Programms beweist oder was verstehst du unter Verifikationssystem?


3)
>
>PS1: "Prädikatenlogische Formel" heißt natürlich nicht "mittels Prädikatenlogik beweisbar".
>
Ja, wie z.B. x=x oder auch durch Quantoren angereicherte Konstrukte.
Warum erwähnst du das ?

>
>Da Programme Schleifen bzw. Rekursion enthalten braucht man Induktion.
>
Ich verstehe nicht, was du damit meinst.
Kannst du mir das genauer (an einem Beispiel erklären)?
was verstehst du unter Induktion ?
Etwa Regelmenge bzw.  induktiv definierte Mengen?

4)
>
>PS2: Was ist denn mit >solchen< Verifikationsalgorithmus gemeint?
>
Das frage ich mich auch.
Uwe Schöning schreibt auf S.120 in „Ideen der Informatik“:

=============================================
Programm A      ---->  | Verifikations- |   A erfüllt S
Spezifikation S ---->  | Algorithmus    |   A ist inkorrekt

Einen solchen Spezifikationsalgorithmus kann es nicht geben.
Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen(als Spezalfall einer Spezifikation, die man in Bezug auf A mach en kann).

===============================================
Vermutlich meint U. Schöningh den Verifikationsalgorithmus

mfg
cx




  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 02.12.2013
Mitteilungen: 212
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, eingetragen 2019-11-29


2019-11-29 11:26 - carlox in Beitrag No. 2 schreibt:
1)
>Ja, das ist eine prädikatenlogische Formel.
>Die kann man hier aber nicht angeben
> Man braucht dazu ja einige Begriffe mittels derer man
>die Spezifikation formulieren kann.
>Allein diese Begriffe formal zu definieren und
>damit dann die Spezifikation als Formel aufzuschreiben ist
>kein einfaches Unterfangen.
>
Das denke ich auch.
Die Spezifikation besteht aus einer Vorbedingung P und einer Nachbedingung Q.
P ist eine prädikatenlogische Formel, die die im Programm A vorkommenden Werte der Variablen vor der Programmausführung betrifft und Q ist eine prädikatenlogische Formel, die die in A vorkommenden Werte der Variablen nach der Programmausführung betrifft.
In einer der in P vorkommenden Variablen (ich nenne sie e) steht dann das zu untersuchende Programm R, also (informal):
e = R
Das zu formalisieren dürfte kein Ptoblem sein: Man nimmt für R einfach die codierte Turingmaschine, die das Programm R darstellt, also eine Zahl.  

In einer der in Q vorkommenden Variablen (ich nenne sie o) steht dann eine Zeichenfolge "R hält an" oder "R hält nicht a" also:
o = "R hält an"  , wenn R anhält  
o = "R hält nicht an"  , wenn R nicht anhält  
Das Problem ist, wie man diese Verzweigung durch eine prädikatenlogische Formel darstellt.
Das dürfte schwierig sein (wie formalisiert man "R hält an" bzw "R hält nicht an"?)    
Oder sehe ich da was falsch ?
Wie ich schon schrieb ist das nicht so einfach. Zunächst muß man ja die Turingmaschine und ihre Arbeitsweise formal definieren und mit diesen Begriffen dann das Halteproblem. Allgemein braucht man irgendein Berechnungsmodell. Nimmt man Turingmaschinen, dann hat man schon verloren. In Termini der Informatik würde man sagen, daß das eine maximal ungeeignete Repräsentation ist. Boyer & Moore haben die Programmiersprache LISP verwendet, genaugenommen PURE LISP.

2019-11-29 11:26 - carlox in Beitrag No. 2 schreibt: 2)
>Boyer und Moore haben die Unlösbarkeit des Halteproblems vor 35 Jahren
>mit ihrem Verifikationssystem bewiesen dl.acm.org/citation.cfm?doid=828.1882 .
>In dem Artikel findet man die Spezifikation - ist aber schwere Kost!  
>
a) Habe versucht den Artikel runterzulade (obwohl ich vermutlich den nicht verstehen werde).
Das kostet Geld  oder gibt es den auch kostenlos?
Hier: www.cs.utexas.edu/users/boyer/unsolv.ps.Z

2019-11-29 11:26 - carlox in Beitrag No. 2 schreibt: 2)
b)
Bis jetzt dachte ich , daß  man unter Programmverifikation (=Verifikationssystem) versteht, dass man die Korrektheit eines konkret vorgegebenen Programms beweist oder was verstehst du unter Verifikationssystem?
Ein Programm mittels dessen die Korrektheit von korrekten Programmen bewiesen werden kann. Solch ein Verifikationssystem ist unvollständig, d.h. es gibt unendlich viele korrekte Programme deren Korrektheit nicht mit dem System bewiesen werden kann. Das folgt aus dem 1. Gödelschen Unvollständigkeitssatz.  

2019-11-29 11:26 - carlox in Beitrag No. 2 schreibt:
3)
>
>PS1: "Prädikatenlogische Formel" heißt natürlich nicht "mittels Prädikatenlogik beweisbar".
>
Ja, wie z.B. x=x oder auch durch Quantoren angereicherte Konstrukte.
Warum erwähnst du das ?
Als Hinweis, daß man Induktion braucht - ohne geht es i. A. nicht.


2019-11-29 11:26 - carlox in Beitrag No. 2 schreibt:
>Da Programme Schleifen bzw. Rekursion enthalten braucht man Induktion.
>
Ich verstehe nicht, was du damit meinst.
Kannst du mir das genauer (an einem Beispiel erklären)?
was verstehst du unter Induktion ?
Etwa Regelmenge bzw.  induktiv definierte Mengen?

Beispielsweise will man

{x ≥ 0} y := 1; while x > 0 do y := x * y; x := x - 1 end {y = x!}

zeigen, d.h. daß mit der while-Schleife die Fakultätsfunktion berechnet wird. Das kann man nur durch Induktion zeigen: Der Schleifenrumpf wird offensichtlich x mal ausgeführt.

Induktionsanfang x = 0: 1 = 0!

Induktionsschritt: Nach x Ausführungen des Schleifenrumps gilt y = x! (Induktionshypothese). Nach x + 1 Ausführungen des Schleifenrumps gilt y = x! *(x + 1) = (x + 1)!

2019-11-29 11:26 - carlox in Beitrag No. 2 schreibt: 4)
>
>PS2: Was ist denn mit >solchen< Verifikationsalgorithmus gemeint?
>
Das frage ich mich auch.
Uwe Schöning schreibt auf S.120 in „Ideen der Informatik“:

=============================================
Programm A      ---->  | Verifikations- |   A erfüllt S
Spezifikation S ---->  | Algorithmus    |   A ist inkorrekt

Einen solchen Spezifikationsalgorithmus kann es nicht geben.
Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen(als Spezalfall einer Spezifikation, die man in Bezug auf A mach en kann).

===============================================
Vermutlich meint U. Schöningh den Verifikationsalgorithmus

Ich verstehe nicht, was mit "Verifikationsalgorithmus" gemeint ist.

Falls ein terminierender Algorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum 1. Gödelschen Unvolsständigkeitssatz.

Falls ein nicht notwendigerweise terminierender Algorithmus gemeint ist, dann erhält man einen Widerspruch zum 1. Gödelschen Unvollsständigkeitssatz.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1025
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, vom Themenstarter, eingetragen 2019-12-04


2019-11-29 15:34 - Zwerg_Allwissend in Beitrag No. 3 schreibt:
Ich verstehe nicht, was mit "Verifikationsalgorithmus" gemeint ist.

Falls ein terminierender Algorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum 1. Gödelschen Unvolsständigkeitssatz.

Falls ein nicht notwendigerweise terminierender Algorithmus gemeint ist, dann erhält man einen Widerspruch zum 1. Gödelschen Unvollsständigkeitssatz.

Hallo Zwerg_Allwissend
Vielen Dank für dein Posting.

Annahme:
Es gibt einen "Verifikationsalgorithmus" :
Programm A      ---->  | Verifikations-   |   A erfüllt S bzw.
Spezifikation S   ---->  | Algorithmus    |   A ist inkorrekt

Im Folgenden will ich zeigen, dass diese Annahme falsch ist.

Man wählt speziell A = Algorithmus, der von einer beliebigen, wahren prädikatenlogischen Formel (ohne freie  Variablen) den Beweis (Beweisfolge) berechnet.
x0, x1, …, xm seien die Variablen des Programms.
Die Werte der Variablen vor der Programmausführung seien:
x0=a_0, x1=a_1, … , xm=a_m
Die Werte der Variablen nach der Programmausführung seien:
x0=e_0, x1=e_1, … , xm=e_m
Es sei
a_0 = alpha , wobei alpha eine beliebige wahre prädikatenlogische Formel (ohne freie Variablen) ist.
b_0 = alpha --> bf
wobei bf eine Beweisfolge (also eine Folge von Formeln) für alpha (d.h. die letzte Fornel in bf ist alpha) ist.
Die Spezifikation S sei wie folgt gewählt:
Vorbedingung P:
[alpha ist eine wahre prädikatenlogischen Formel (ohne freie  Variablen)] ist wahr.
Nachbedingung Q:
[alpha --> bf] ist wahr
Da dies dem 1. Gödelschen Unvollständigkeitssatz widerspricht, ist die obige Annahme falsch.

Frage:
Ist meine Argumentation richtig ?

Problem:
Die Vorbedingung P und die Nachbedingung Q ist nicht in PL1 (Prädikatenlogik 1. Stufe) formalisiert.
Wie kann man das machen ?

PS:
Was mir dazu nachträglich noch einfällt (wie man es "hinbiegen kann"):
Man kann eine Formel durch eine Zahl codieren.
Genauso kann man eine Beweisfolge durch eine Zahl codieren.
Die prädikatenlogische Formel Fz (wobei z eine Konstante ist) wird dann interpretiert als:
Die zu z zugehörige Zahl ist eine Formel.
Die prädikatenlogische Formel Bz (wobei z eine Konstante ist) wird dann interpretiert als:
Die zu z zugehörige Zahl ist eine Beweisfolge.


mfg
cx





  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 02.12.2013
Mitteilungen: 212
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.5, eingetragen 2019-12-04


2019-12-04 12:04 - carlox in Beitrag No. 4 schreibt:
Programm A      ---->  | Verifikations-   |   A erfüllt S bzw.
Spezifikation S   ---->  | Algorithmus    |   A ist inkorrekt

Was soll das bedeuten?



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1025
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.6, vom Themenstarter, eingetragen 2019-12-05



Programm A      ---->  | Verifikations-   |   A erfüllt S bzw.
Spezifikation S   ---->  | Algorithmus    |   A ist inkorrekt

>
>Was soll das bedeuten?
>




Zitat: (S.121-122) "Ideen der Informatik" von U. Schöning:
====================================
Das Problem der Programmverifikation ist das Folgende:
Gegeben ist ein auf Korrektheit zu analysierenes Programm A.
Was es genau heißt, korrekt zu sein, also die Wunschvorstellung, die man von dem Programm A hat, wid formal spezifiziert in eine Spezifikation S. Dies ist eine Ansammlung von Formeln (vgl. Kapitel 5), die Aussagen darüber machen, welche Eigenschaften die im Programm A vorkommenden Variablen nach der Ausführung des Programms A haben sollten - unter Bezugnahme auf die Werte der Variablen, die vor Ausführung des Programms A galten. Die Wunschvorstellung wird durch folgendes Bild dargestellt:

                                   +---------------+    
Programm A      ---->  | Verifikations-   | --> "Prog. A erfüllt Spez. S"
Spezifikation S   ---->  | Algorithmus    | --> "Prog. A ist inkorrekt"
                                   +---------------+

Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann).
====================================

mfg
cx




  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 02.12.2013
Mitteilungen: 212
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.7, eingetragen 2019-12-05


2019-12-05 10:29 - carlox in Beitrag No. 6 schreibt:

Programm A      ---->  | Verifikations-   |   A erfüllt S bzw.
Spezifikation S   ---->  | Algorithmus    |   A ist inkorrekt

>
>Was soll das bedeuten?
>




Zitat: (S.121-122) "Ideen der Informatik" von U. Schöning:
====================================
Das Problem der Programmverifikation ist das Folgende:
Gegeben ist ein auf Korrektheit zu analysierenes Programm A.
Was es genau heißt, korrekt zu sein, also die Wunschvorstellung, die man von dem Programm A hat, wid formal spezifiziert in eine Spezifikation S. Dies ist eine Ansammlung von Formeln (vgl. Kapitel 5), die Aussagen darüber machen, welche Eigenschaften die im Programm A vorkommenden Variablen nach der Ausführung des Programms A haben sollten - unter Bezugnahme auf die Werte der Variablen, die vor Ausführung des Programms A galten. Die Wunschvorstellung wird durch folgendes Bild dargestellt:

                                   +---------------+    
Programm A      ---->  | Verifikations-   | --> "Prog. A erfüllt Spez. S"
Spezifikation S   ---->  | Algorithmus    | --> "Prog. A ist inkorrekt"
                                   +---------------+

Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann).
====================================

Ich hatte ja schon in #3 geantwortet:

Falls ein terminierender Verifikationsalgorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum 1. Gödelschen Unvolsständigkeitssatz.


Dein Beipiel aus #4 ist viel zu kompliziert:

Nehme eine Programmiersprache Deiner Wahl, definiere darin die natürlichen Zahlen, die Addition + und die Multiplikation * darauf. Dann hast Du ein Fragment der Arithmetik. Unter den unendlich vielen wahren Aussagen über + und * gibt es nach dem 1. Gödelschen Unvollständigkeitssatz unendlich viele, die ein korrektes Verifikationssystem für die Programmiersprache nicht beweisen kann.

Es gibt inzwischen viele, im freien Download erhältliche, Beweissysteme mit denen man Programme verifizieren kann. Diese Systeme sind notwendigerweise alle unvollständig. Die Systeme sind "interaktiv", d.h. wenn der Beweiser eine Aussage nicht beweisen kann, dann kann der Benutzer  dem System "helfen". Beweise von einfachen Aussagen, wie Assoziativität, Kommutativität und Distributivität von + und * gelingen automatisch.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1025
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.8, vom Themenstarter, eingetragen 2019-12-09


Hallo ZA,

1)

Ich hatte ja schon in #3 geantwortet:
Falls ein terminierender Verifikationsalgorithmus gemeint ist, dann erhält man nicht nur einen Widerspruch zum Satz von Rice, sondern auch zum
1. Gödelschen Unvolsständigkeitssatz.

Ich will diesen Widerspruch zeigen unter den Voraussetzungen, die Schöning macht: (siehe die entsprecheden Zitate in diesem Thread):
"Einen solchen Spezifikationsalgorithmus kann es nicht geben. Insbesondere würde er dem Satz von Rice widersprechen. Ein solcher Verifikationsalgorithmus könnte das Halteproblem lösen (als Spezialfall einer Spezifikation, die man in Bezug auf A machen kann)."

D.h. man muß eine Spezifikation S zu A angeben.
wobei A = Algorithmus, der von einer beliebigen, wahren prädikatenlogischen Formel (ohne freie  Variablen) den Beweis (Beweisfolge) berechnet.
Wie kann man diese Spezifikation S formalisieren ?
bzw. wenn es diese Spezifikation S geben würde, warum gibt dann es einen Widerspruch zum Satz von Rice ?

2)

Dein Beipiel aus #4 ist viel zu kompliziert:
Ist es aber korrekt ?

mfg
cx








  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 02.12.2013
Mitteilungen: 212
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.9, eingetragen 2019-12-10


Das Buch von Herrn Schöning kenne ich nicht. Für weiteres fehlen mir daher die Details. Z.B. habe ich den Begriff "Spezifikationsalgorithmus" noch nie gehört. Am besten fragst Du ihn selbst (per Email). Ob Deine Beweisskizze aus #4 korrekt ist weiß ich nicht, ist mir zu kompliziert zum Nachrechnen.



  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1025
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.10, vom Themenstarter, eingetragen 2019-12-11


2019-12-10 11:42 - Zwerg_Allwissend in Beitrag No. 9 schreibt:
Das Buch von Herrn Schöning kenne ich nicht.
Die Bücher von U. Schöning sind wirklich gut!


Für weiteres fehlen mir daher die Details. Z.B. habe ich den Begriff "Spezifikationsalgorithmus" noch nie gehört. Am besten fragst Du ihn selbst (per Email). Ob Deine Beweisskizze aus #4 korrekt ist weiß ich nicht, ist mir zu kompliziert zum Nachrechnen.

Ich werde versuchen, ihn per email zu kontaktieren.

mfg
cx



  Profil  Quote  Link auf diesen Beitrag Link
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox wird per Mail über neue Antworten informiert.
Neues Thema [Neues Thema] Antworten [Antworten]    Druckversion [Druckversion]

 


Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2019 by Matroids Matheplanet
This web site was made with PHP-Nuke, a web portal system written in PHP. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]