# Natural Normal Form

In natural logic, the following program:

``a(u).if (a(v))  b(v).c(z).not d(z).either e(z) or f(z).for (let every x: a(x))  b(x).``

Gets parsed as follows:

That form maps very closely the syntax, but needs to be preprocessed to help us make deductions effectively.

First, all `if`s are inverted. For example, the following:

Normalize ➩

Negations are simplified by altering the value of the node:

Normalize ➩

Either-ors are simplified by making two statements, one for each possibility:

Normalize ➩

For loops are simplified by making the variables quantified:

Normalize ➩

This is done recursively, so if you have a lot of nesting it gets flattened:

Normalize ➩

Or a long condition:

Normalize ➩

The entire original program, when it goes through this process, gets simplified to be the following:

Which is somewhat equivalent to the following horn-clause-like statements:

``a(u).b(v) if (a(v)).c(z).not d(z).e(z) if not f(z).f(z) if not e(z).let every x: b(x) if a(x).``