++ Mathe Formeln ++ Mathematik Lexikon ++ Lösungen ++ Hausaufgaben ++ Algebra ++ Lernen ++ Übungen ++ Schule ++ Geometrie ++

Navigation

Mathematik Begriffe
A B C D E
F G H I J
K L M N O
P Q R S T
U V W X Y
Z 123      
Goldkurs

Mathematik Begriff Erklärung Algorithmus von Gilmore Formel Hilfe Hausaufgabeb
Algorithmus von Gilmore

Der Algorithmus von Gilmore basiert auf dem Satz von Herbrand und liefert ein Semi-Entscheidungsverfahren um prädikatenlogische Formeln auf Unerfüllbarkeit zu testen. Es gilt:

Gilmore\left(E\left(F\right)\right)=\begin{cases}halt, & \mbox{wenn }F\mbox{ unerfüllbar} \\ undef, & \mbox{wenn }F\mbox{ erfüllbar} \end{cases}
mit E(F) sei die Herbrand-Expansion von F.

 

Verfahren

Die Menge E(F) mit

E\left(F\right)=\left\{A_1, A_2, ...\right\}

sei die Herbrand-Expansion zu F.

i = 1;
prüfe A1 = :temp auf Unerfüllbarkeit (aussagenlogisch);

WHILE {

prüfe temp \wedge A_{i+1} =: temp auf Unerfüllbarkeit (aussagenlogisch)
wenn Unerfüllbar, dann halt, i++ sonst;

}
Dieser Artikel ( Algorithmus von Gilmore ) stammt aus Wikipedia, der freien Enzyklopädie
und steht unter der GNU Free Documentation Licence. 
+++ Mathe Formeln ++ Mathematik Lexikon ++ Lösungen ++ IMPRESSUM ++ Algebra ++ Lernen ++ Übungen ++ Schule ++ Geometrie +++