Posted on January 6, 2018 and last updated on January 27, 2018 by Mistral Contrastin

Logic and Proof Example Sheet I

From the lecture notes

Exam questions


Write a program to convert an arbitrary propositional logic formula to CNF. Formulae involve single capital letter variables and the following operators:

To prevent you from losing time on parsing you can use prefix notation.

Example input from shell: or (and P Q) R Example output to shell: and (or P R) (or Q R)

Bonus points if you implement a theorem prover on top of it. (It is not as difficult as it sounds.)

Please write it in one of the following languages: Haskell, SML, OCaml, Prolog, Elixir, Ruby, Python, Fortran, C, C++, Java, Scheme, Common Lisp.

You will realise it is much easier to do it in functional languages compared to procedural ones.