Diskussion:Algorithmus von Gilmore

aus Wikipedia, der freien Enzyklopädie
Letzter Kommentar: vor 9 Jahren von 78.51.205.211 in Abschnitt Terminologie
Zur Navigation springen Zur Suche springen

Ich galube der erste Fall in der Gilmore-Funktion sollte falsifizierbar und nicht unerfüllbar heißen, weil um die Unerfüllbarkeit zu beweisen, muss man alle Elemente der Herbrand-Expansion durchprobieren. Da das Herbrand-Universum und dementsprechend die Herbrand-Expansion i.A. abzählbar unendlich sind, wird der Algorithmus i.A. nicht terminieren. Vielmehr wird er beim ersten Konjunkt, der als FALSE ausgewertet wird, terminieren und somit nachweisen, dass die Klauselmenge falsifizierbar (wass automatisch nicht allgemeingültig heißt) ist.

Terminologie

[Quelltext bearbeiten]

Der Satz „Man sieht, dass der Algorithmus semi-entscheidbar ist“ ist meines Erachtens nicht ganz sauber formuliert. Semi-Entscheidbarkeit ist Eigenschaft eines Problems, nicht eines Algorithmus: Ein (Entscheidungs-)Problem heißt (genau dann) semi-entscheidbar, wenn es einen Algorithmus gibt, der für jedes in endlicher Zeit hält und für alle nicht terminiert. Ein Problem kann also auch entscheidbar sein, obwohl ein bestimmter Algorithmus es nur semi-entscheidet.

Man müsste also eigentlich formulieren: „Man sieht, dass der Algorithmus das Unerfüllbarkeitsproblem nur semi-entscheidet, da er nur in endlicher Zeit hält, wenn er Unerfüllbarkeit feststellt. Da das prädikatenlogische Unerfüllbarkeitsproblem nicht entscheidbar ist, kann es auch keinen stets terminierenden Algorithmus geben, der diese Entscheidung leistet.“

Signatur vergessen. --78.51.205.211 18:51, 8. Feb. 2015 (CET)Beantworten