Natural Normal Form
In natural logic, the following program:
either e(z) or f(z).
for (let every x: a(x))
Gets parsed as follows:
That form maps very closely the syntax, but needs to be preprocessed to help us make deductions effectively.
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:
b(v) if (a(v)).
e(z) if not f(z).
f(z) if not e(z).
let every x: b(x) if a(x).