Thursday, January 12, 2006

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.

Tuesday, January 10, 2006

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.