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.

Plans

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

• Tuesday 10am, to discuss Graph-based Algorithms for Boolean Function Manipulation by Bryant
• Wednesday 2pm, to discuss ModGen: Theorem Proving by Model Generation by Kim and Zhang
• Friday 10am for a final review

CTL example

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

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.

mu-calculus and CTL

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

mu-calculus and CTL

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

mu-calculus and CTL

Introduction to translation from CTL to modal mu-calculus.

Assignment 1 released

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

NuSMV

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

• User Manual
• Tutorial
• Foils
• A copy of the NuSMV binary is available on DICE at /home/mfourman/bin/NuSMV

Temporal Logic: CTL

Stuttgart CTL Notes

Finite State Machines

STRIPS planning

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

STRIPS

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

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

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

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

CNF: Davis Putnam and variations

Sebastiani CADE 04 Slides pp. 25 - 28, 38 -52
Propsat Demonstration

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.

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.