Logic and Verification

Lecture: Wednesdays 10.15-12.15, room 139.
Exercise: Wednesdays 12.15-14.15, room 140.


The lecture consists of 4 parts.

Exercise with Circuit Verification, for 25th of March

Some material for the exercise: The satsolver, the CNF convertor, the specification of the adder with lookahead carry generation, the specification of addition through the two-complement method. The task was to prove that for the addition circuits holds: ( x + y ) - y = 0, and to verify the circuit in which look ahead carry is computed in groups of two. The CNF converter produces a lot of junk output. The clauses are at the end.

HOL Light System

Here is the exercise for 1st of April and these are the slides about Church's type theory. If you want to read a bit more about the HOL system, I recommend the manual . (It is more than just a manual)