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.

Wednesday, March 16, 2005


Following discussion in class yesterday, there will be no further meetings this week.

Because I was unable to provide you with materials last week, there is no longer time for you to prepare oral presentations, so your oral presentation has been CANCELLED. Instead we will discuss two key papers in class. You should prepare for these classes by reading the papers, identifying the key ideas they introduce, and noting some questions for discussion.

Next week we will meet on

Thursday, March 10, 2005

CTL example

Computing interpretations of CTL formulae for a simple example with four states.

Sunday, March 06, 2005

Assignment 1 Submission

The correct command for this should be submit msc propm 1 Apologies that this is past the deadline - if you have not already submitted (or wish to resubmit) please do so by 0900 tomorrow 7th March.

Thursday, March 03, 2005

mu-calculus and CTL

Ch 6 of Model Checking No lecture 8th March. Meet instead on Wednesday 9th 2pm.

Tuesday, March 01, 2005

mu-calculus and CTL

  • Syntax and Semantics
  • Monotone operators
  • EG f = nu Q. f /\ EX Q
  • EF f = mu Q. f \/ EX Q

Friday, February 25, 2005

mu-calculus and CTL

Introduction to translation from CTL to modal mu-calculus.

Tuesday, February 15, 2005

Assignment 1 released

The assignments page has the details.
Now with the corrected link!
Deadline changed - now 2400 4th March 2005!

Friday, February 11, 2005


NuSMV is a symbolic model checker. NuSMV2, combines BDD-based model checking and SAT-based model checking.

Tuesday, February 08, 2005

Temporal Logic: CTL

Friday, February 04, 2005

Finite State Machines

Tuesday, February 01, 2005

STRIPS planning

Recap of SAT and phase transition Zhang slides part 1 pp. 26-36.


  • PropPlan
  • Actions, preconditions postconditions.
  • Frame problem
  • Logical formulation using quantified boolean formula (QBF)

Friday, January 28, 2005

k-SAT => 3-SAT; intro to ML

Exercise 1 is available online, as are the ML examples.

Tuesday, January 25, 2005

Binary Decision Diagrams/SAT Phase Transition

Binary Decision Diagrams
Bryant '92
Sebastiani CADE 04 Slides pp. 53-58
Phase Transition
Sebastiani CADE 04 Slides pp. 29-37

Friday, January 21, 2005

CNF: Davis Putnam and variations

Friday, January 14, 2005

Propositional Logic Review

Topics Covered (Sebastiani CADE 04 Slides pp. 8-24)
Boolean Propositional Logic
Connectives, Valuations, Truth Tables
Trees and DAGs
Best-case exponential saving in space and time.
Normal Forms
Negative Normal Form
expand implications; push negations down using de Morgan and double negation
Conjunctive Normal Form
Distribute \/ over /\, top-down. Worst-case exponential.

First Lecture Today!

Apologies for the timetabling confusion yesterday. We meet regularly on Tuesdays and Fridays 10am room 5.01 Appleton Tower. Today I will review propositional and first-order logic, and demonstrate propsat, an online tool that uses a propositional representation to model and reason about first-order theories over finite domains. Comments on this blog are welcome from both students and kibbitzers on the www.

Saturday, December 18, 2004

Subscribe to the Atom Feed

I plan to use this Blog to keep you up-to-date, and to keep a record of the course. If you use Firefox, you can use the orange button in the status bar to create a live bookmark to the feed—use the Sage extension to manage feeds. You can then use this to alert you to new blog entries.

Alternatively, students should use an "Atom Reader" such as NewsFire for Mac OSX (search Google to find one for your OS), to subscribe to the Atom Feed associated with the course.