These tests ensure that multiple negations are eliminated, negated
quantifiers are replaced appropriately, negations introduced by
reduction are correctly handled, and negated disjunctions and
conjunctions are replaced according to De Morgan’s rules.
These tests ensure that universal quantifiers are correctly reduced to
negated existential quantifiers over the negated argument via derived
predicates in preconditions (nested and not) and goal descriptions.
Patrick Lühne