Diskussion:Algorithmus von Gilmore

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

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 $P$ heißt (genau dann) semi-entscheidbar, wenn es einen Algorithmus gibt, der für jedes $x\in P$ in endlicher Zeit hält und für alle $x\notin P$ 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)