Skolemisierung

Einfache Sprache

Die Skolemisierung macht aus einer Prädikatenlogische Formel in PNF eine Formel in SNF.

Def. Skolemisierung

Algorithmus

  	\begin{algorithm}
	\caption{Skolem}
	\begin{algorithmic}
	\Input $\varphi = Q_0x_{i_0}\ldots Q_{n-1}x_{i_{n-1}}\psi\in\mathbf{PNF}$
	\Output Formula in $\mathbf{SNF}$
	\State $j\gets 0$
	\While{$j<n$}
		\If{$Q_j = \forall$}
			\State $j\gets j+1$
        \Else
	        \State $\{x_{l_0},\ldots,x_{l_m}\} \gets \mathrm{fvars}(Q_jx_{i_j}\ldots Q_{n-1}x_{i_{n-1}})$
		    \State $\chi\gets Q_{j+1}x_{i_{j+1}}\ldots Q_{n-1}x_{i_{n-1}}\varphi\{x_{i_j}\mapsto f(x_{l_0},\ldots,x_{l_m})\}$ with $f$ being a $m$-stellige function 
			\State $j\gets j+1$
        \EndIf
    \EndWhile

	\end{algorithmic}
	\end{algorithm}