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))