# Natural Normal Form

Sam Goto

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:

Negations are simplified by altering the value of the node:

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

For loops are simplified by making the variables quantified:

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

Or a long condition:

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).