NNF for non-empty trace vs empty-trace semantics

[marfvr]

This issue is to keep track of a discrepancy between NNF with empty-trace and non-empty trace semantics.

For example, let us denote ~ the logical not and ! the propositional not. Also, let a be an atom.

The NNF of a is a in both semantics.
The NNF of !a is !a in both semantics.
The NNF of ~a should be !a | end for empty-trace sem., and !a for non-empty trace sem.
The NNF of ~!a should be a | end for empty-trace sem., and a for non-empty trace sem.