Prenexificação.

A expansão de Herbrand H(T) dum conjunto de fórmulas fechadas universal T. Começo da demonstração de que T é satisfazível sse H(T) é proposicionalmente satisfazível.