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";;