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.

CNF, SAT and the phase transition

Sebastiani slides to p. 30

• Propositional Logic
• Valuations and Semantics
• Equivalence, Satisfiability and Equi-Satisfiability
• CNF; labelling CNF; 3-CNF
• Phase Transition: satisfiability, complexity.

Future meetings will be held in AT 3.03

Session 2005-2006

The calendar of meetings, deadlines, etc. for this class can be found at .ics  html

Class announcements will be made via this Blog.