#2 Incorrect Conversion of Double 'not' to CNF

[Nick R]

When I attempt to convert a clause that contains a double 'not' to CNF using NotExp.toConjunctiveNormalForm(), it is incorrectly simplified to a single 'not'. I have seen this issue in both the simple example below and anytime I convert an ImplyExp that contains a 'not' on the left hand side of the equation into CNF.

Per the API, the .toConjunctiveNormalForm() method first converts the expression into negative normal form. The API for the Exp.toNegativeNormalForm() correctly states that the following conversion should be performed:
(not (not F)) => F

I have tried to avoid this problem via several different combinations of AtomicFormulas, NotAtomicFormulas, and NotExps, but all consistently provide the incorrect simplification of a double 'not'.

Below I've included a snippet of code that illustrates this example:

import pddl4j.exp.*;

public class testpddlparser {
public static void main (String[] args) {
// Test Variables
AtomicFormula afA = new AtomicFormula("A");
NotExp notExp_afA = new NotExp(afA);
NotExp notNotExp_afA = new NotExp(notExp_afA);

System.out.println("1) AtomicFormula : " +afA);
System.out.println("2) NotExp of AtomicFormula : " +notExp_afA);
System.out.println("3) Double NotExp of AtomicFormula: " +notNotExp_afA);
System.out.println("4) Double NotExp as CNF : " +notNotExp_afA.toConjunctiveNormalForm());
}
}

Output:
1) AtomicFormula : (A)
2) NotExp of AtomicFormula : (not (A))
3) Double NotExp of AtomicFormula: (not (not (A)))
4) Double NotExp as CNF : (and (not (A)))

Thank you,

Nick