Introduction to ML

Standard ML is a programming language ideally adapted to representation and manipulation of logical expressions. We introduce ML with a straightforward representation of propositional formulae and a naive attempt at implementing reduction to CNF.

Implementation of a correct, complete, and efficient CNF reduction is set as an exercise.