# Logic and Verification

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

## Overview

The lecture consists of 4 parts.
• Propositional Logic. I explain the Davis-Putnam-Logemann-Loveland algorithm, which is the best-known technique for solving propositional logic. We will use DPLL for solving sudokus and other puzzles. We will also try to do some serious things. (Like proving correctness of Boolean circuits for addition)
• First-order techniques. I will probably explain Geometric resolution. Usefullness of TPTP.
• HOL light system. Homepage of the system.
• Coq proof assistent. Here is the homepage.

## 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)
• Slides about how to define inductive types and predicates, and how to derive elementary properties of inductive types and predicates.
• A list of HOL commands that I used in the examples.
• Proof of commutativity of addition , and some proofs involving lists . Try to prove some properties of even and odd for the next time: Every number is either odd or even. No number is both odd and even.
• This is the file for clause logic that we prepared in class. Define a notion of implication for a clauselist and a clause, and for a clauselist and a clauselist.
• This is the final verification of the DPLL algorithm. In order to run the proof, download all the files and type #use "script.ml";;