CNF reduction in ML

Exercise 1: Reduction to CNF - a first exercise in ML

Issued 12 January 2005


In this assignment you will gain some familiarity with the programming language ML and implement a non-trivial CNF reduction.


The ML recommended for this course is Dave Matthews' PolyML, which is freely available for download for a number of platforms. The PolyML site also includes useful documentation.

PolyML is installed on DICE machines and is invoked with the shell command "poly". Alternatives include "Moscow ML" and "Standard ML of New Jersey", which implement the same language (for our purposes at least), and can be tracked down using Google.



  1. The example file CNF conversion in ML provides a partial implementation of the naive CNF conversion (Sebastiani p.24). Read and understand the code. Look at the warnings generated when you compile (ie "use") this file. Test this on a number of example formulae, and complete any missing cases.
  2. Implement the labelling CNF conversion (Sebastiani p.25).
    You will probably find the following code snippet useful.

    val gensym = let val count = ref 0 in fn () => (count := !count +1; "X"^(Int.toString (!count))) end

    (Repeated evaluations of gensym() generate a sequence of strings "X1", "X2", etc. which can be used as names of new variables.)

  3. (Optional) Implement the improved labelling CNF conversion (Sebastiani p. 27)

Author: Michael Fourman
Revision 1.5 by MichaelFourman
2006/01/12 09:16:07

Home : Teaching : Courses : Propm : Assignments 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail:
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh