Prenex normal form

The prenex form is a possible normal form, can be represented in the statements of predicate logic. It is required, among other things as a precursor to Skolem.

A statement in the first order predicate logic is in prenex form if all quantifiers ( descriptions of the scope ) outside or prior to the actual formula,. Contains the prenex additionally only conjunction, disjunction and negation (immediately before atoms) as connectives, it is also known as technical negation normal form.

In QL, there are at any one formula logically equivalent formula in prenex form.

A formula in prenex adjusted is satisfiable if their Skolem is satisfiable.

Mathematical definition

A formula F of the predicate calculus is in prenex form if it of the form

Is that

In no quantifier may occur.

Means prefix is the matrix.

Example

The output formula is:

It is the variable y before both bound and free. But this must not be in prenex form. Therefore, a new variable is introduced: w. After the adjustment, it looks like this:

Now each variable is either bound or free before and thus we can use the quantifiers "pull" all forward, which then looks as follows:

• Logic