Prädikatenlogik: Beweis rekursive Aufzählbarkeit

22.05.2012, 20:49	LiGo	Auf diesen Beitrag antworten »
Prädikatenlogik: Beweis rekursive Aufzählbarkeit Aufgabe: Es sei $\begin{eqnarray} \tau \end{eqnarray}$ ein rekursiver Typ. Beweisen oder widerlegen Sie: $\begin{eqnarray} \{ \alpha \in PF \mid \alpha \end{eqnarray}$ ist erfüllbar $\begin{eqnarray} \} \end{eqnarray}$ ist rekrursiv aufzählbar. Lösungsansätze / Ideen: Ich denke, dass die Behauptung stimmt, da bei einem rekursiven Typ es auch möglich sein sollte, die die erfüllbaren Funktionen für den Typ aufzuzählen. Ich denke ausserdem, dass man ein Verfahren braucht, dass für eine gegebene Formel $\begin{eqnarray} \alpha \end{eqnarray}$ hält, wenn $\begin{eqnarray} \alpha \end{eqnarray}$ erfüllbar ist, sonst nicht. Genau für dieses Verfahren fehlt mir aber völlig der Ansatz
23.05.2012, 18:07	kiste	Auf diesen Beitrag antworten »
Hallo, ich kenne mich mit rekursiven Typ oder so nicht aus, aber die Herbrand-Theorie liefert einen Semientscheidbarkeits-Algorithmus für das Erfüllbarkeitsproblem der Prädikatenlogik.
23.05.2012, 22:32	LiGo	Auf diesen Beitrag antworten »
Ok, dass würde bedeuten, dass man diesen Algorithmus in ein Verfahren packen und dnn könnte man die erfüllbaren Formeln für den rekursiven Tyen aufzählen. Kann das jemand bestätigen? Und kennt jemand diesen Algorithmus näher? Ich kann nchts darüber finden.

1

Verwandte Themen

Die Beliebtesten »

Die Größten »

Die Neuesten »