PROGRAM VERIFICATION

Handout #3


How can one establish that the following symbolic manipulation process always terminates with a formula in disjunctive normal form?
 
 

BEFORE
AFTER
not(not(x))
x
not(and(x,y))
or(not(x),not(y))
not(or(x,y))
and(not(x),not(y))
and(x,or(y,z))
or(and(x,z),and(y,z))
and(or(y,z),x)
or(and(z,x),and(z,y))

These transformations can be applied in any order anywhere in a given formula, and are continued until none is applicable.