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