1

I am using Dr Racket to check if an expression passed is in Conjunctive normal form.

The code checks if the expression is in Negative normal form first.

(define (is-nnf? expr)
  (cond
   [ (is-constant? expr) #t ]
   [ (is-variable? expr) #t ]
   [ (is-not? expr) (is-variable? (op1 expr)) ]
   [ (is-or? expr) (and (is-nnf? (op1 expr)) (is-nnf? (op2 expr))) ]
   [ (is-and? expr) (and (is-nnf? (op1 expr)) (is-nnf? (op2 expr))) ]
  ) 
)

is-nnf checks recursively whether the expression is in negative normal form.

I am trying to write a similar expression named is-cnf to recursively check if an expression is in conjunctive normal form.

is-constant -> checks if the expression is a constant (Eg #t, #f)

is-variable -> checks if the expression is a variable (Eg 'a, 'x)

is-not -> checks if the first element of the list is a 'not ( Eg. '(not x))

is-or -> checks if the first element of the list is a 'not ( Eg. '(or x y))

is-and -> checks if the first element of the list is a 'not ( Eg. '(and x y))

4

0 回答 0