No woman sleeps.

Naive LF:

no'(e0, w, e1, e2) & woman'(e1,w) & sleep'(e2, w)
     & Rexist(e2)

Coerce claim of sentence from e2 to e0 thru "no" relation:

Rexist (e0)

Axiom in KB defining "no" predicate:

no(w e1 e2)
     <--> (A w1,e3,e4)
                 [subst(w, e1, w1, e3) & subst(w, e2, w1, e4)
                    & Rexist(e3)  -->  ~Rexist(e4)]
subst(a,b,c,d): A substitution operator: a plays the same role in b 
      that c plays in d.  Here, c and d are instances of a and b,    
      resp.

What I'm unhappy about:  the e2 argument of "no".  I'd prefer 
no(w,e1) in the naive logical form, with some kind of pragmatic strengthening converting that to no(w,e1&e2).  (This is what I did in my paper "Monotone Decreasing Quantifiers" for the example "Few men work", where I strengthened the plural morpheme to the set defined by e1&e2.  But here there's no plural morpheme to strengthen.

In this case the axiom defining "no" would be

   no(w,e) 
      <-->  (A w1,e1) subst(w,e,w1,e1) --> ~Rexist(e1)