[DL] validity of laws of predicate logic under CWA and NAF

[Ankesh Khandelwal]

Dear DL-members,

I have a knowledge base and a set of rules written under closed world
assumption that use negation only as negation as failure.

Under these circumstances are the laws of quantifier movement valid?
Laws of Quantifier movements:
1. '(all x.P(x)) --> Q' equivalent-to 'exists x.(P(x)-->Q)', provided x is
not free in Q
2. '(exisits x.P(x)) --> Q' equivalent-to 'all x.(P(x)-->Q)', provided x
is not free in Q
3. 'P --> (all x.Q(x))' equivalent-to 'all x.(P --> Q(x))', provided x is
not free in P
4. 'P --> (exists x.Q(x))' equivalent-to 'exists x.(P --> Q(x))', provided
x is not free in P

And/ Or are the following laws valid?
1. 'not(all x. P(x))' equivalent-to 'exists x.(not P(x))', where not has
the Negation as Failure semantics.
2. 'not(exists x. P(x))' equivalent-to 'all x.(not P(x))', where not has
the Negation as Failure semantics.

Thank you,
Ankesh