Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Automated Reasoning 2005/2006
Automated Reasoning 2005/2006
This page is updated regularly.
Always consult the most recent version.
General
This course is part of the Master programs Computing Science and Artificial
Intelligence. It is given in the first half of the first semester (September to
November). It is a 5 ECTS course.
Teachers
Wim H. Hesselink
Gerard R. Renardel de Lavalette
Prerequisites
Discrete Structures and Knowledge Representation (from the bachelor program
Computing Science), or
Introduction to Logic and Advanced Logic (from the bachelor program Artificial
Intelligence).
Course description
Reasoning is the ability to make inferences, and automated
reasoning is concerned with the design of computing systems that automate,
support, or verify this process. This course gives an introduction into
this active field of research. It consists of two parts: theorem proving
and model checking. A theorem prover assists the user to construct and
check proofs. A model checker allows the user to check whether certain
properties hold in a model that the user defines. We shall use the theorem prover
PVS and the model checker SPIN.
Students will be engaged with the practice of
automated reasoning by assignments: providing
proofs, designing models, and
inferring, verifying and falsifying properties of those models.
Time and place
Monday 9.15--11 h.: lecture in room 210, Blauwborgje 10
Thursday 11:15 -13 h.: computer lab session in room IWI 9, Blauwborgje 3
Friday 9.15--11 h.: lecture in room 210, Blauwborgje 10
Examination
Practical assignments and a written exam.
Links
Som useful links:
Week schedule (preliminary, consult the latest version!)
Week 1 (Monday 5 September 2005 - Friday 9 September 2005)
Lecture 1: preliminaries. Naive set theory, relations and functions, predicate
logic, sequent calculus, lambda calculus.
See the handout.
Lecture 2: first encounter with PVS. Relevant files: trans.pvs and pvs_help. It is useful to have a printout of these files with you at the lecture.
Assignment 1: deadline Friday, September 16,
2005, 17.00 h.
Week 2 (Monday 12 September 2005 - Friday 16 September 2005)
Lecture 3: The logic of PVS (Chapter 3 of the PVS Prover guide); examples of proofs and proof commands (Chapter 4 of the PVS Prover guide).
Computer lab session on Thursday, September 15, 11.15 - 13 h., room IWI 9.
Lecture 4: on Friday, September 16, 9.15 - 11 h., room BB10 0210. Proving correctness of sequential programs in PVS. Binary Search, swapping array elements.
As a preparation, copy the binary search dump file to a new directory, call pvs, undump the file, print only the files binsearch.pvs and programs.pvs and take them with you to the lecture.
Assignment 2: deadline Wednesday, September 21, 2005, 17.00 h.
Week 3 (Monday 19 September 2005 - Friday 23 September 2005)
No lecture on Monday, September 19.
Computer lab session on Thursday, September 22, 11.15 - 13 h., room IWI 9.
Friday, September 23: lecture 5, proving correctness of concurrent programs in PVS. Peterson's mutual
exclusion program, mutual exclusion with one binary semaphore. See the handout.
Assignment 3: deadline Tuesday, October 4, 2005, 17.00 h.
Week 4 (Monday 26 September 2003 - Friday 30 September 2005)
Lecture 6: temporal logic. Modal logic, Kripke models, the temporal logics CTL*,
CTL, LTL: see the handout. There is also another
handout with a few copies from Chapter 2 and 3 of the book Model Checking
by Clarke, Grumberg and Peled.
Lecture 7: temporal logic and model checking.
Week 5 (Monday 3 October 2005 - Friday 7 October 2005)
Lecture 8: first encounter with SPIN and the language Promela. See the Introduction to the Model Checker Spin, the Concise Promela reference by
Rob Gerth, and the file with some introductory Promela scripts.
Computer lab session on Thursday, October 6, 11.15 - 13 h., room IWI 9.
[No second lecture this week.]
Assignment 4: deadline Friday, October 14, 2005,
17.00 h.
Week 6 (Monday 10 October 2005 - Friday 14 October 2005)
Lecture 9: Berman and Garay's algorithm
for fault-tolerant consensus. See Exercise 1.3 in the Exercise Series from Twente University.
[No second lecture this week.]
Assignment 5: deadline Friday, October 28, 2005,
17.00 h.
Week 7 (Monday 17 October 2005 - Friday 21 October 2005)
Lecture 10 (final lecture). Working with Spin: acceptance en progress (see the handout). LTL formulae interpreted as finite automata. Queueing semaphore.
Exam: Monday, November 7, 14 - 17 h., Examenhal
See the exams of previous years (the first two are in Dutch):October 2003, February 2004, November 2004, February 2005.
Gerard Renardel
(grl@cs.rug.nl)