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.
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, letabe an atom.The NNF of
aisain both semantics.The NNF of
!ais!ain both semantics.The NNF of
~ashould be!a | endfor empty-trace sem., and!afor non-empty trace sem.The NNF of
~!ashould bea | endfor empty-trace sem., andafor non-empty trace sem.