Nonstandart logics

Lecturer:

Tutor:

Supervisor:

Department of Mathematics

Synopsis:

The lecture is devoted to modern branches of mathematical logic

that are useful in computer science: modal and temporal logics

as means for program correctness analysis. We stress the algebraic

side of logics: we introduce Boolean, modal and temporal algebras

and show how to use them in logic. We will briefly sketch other

possible relevant generalizations of classical logic: intuitionism

and type theory.

Requirements:

The requirement for receiving the credit is an active participation in the tutorials.

Syllabus of lectures:

1. Possibilities of classical propositional and predicate logics.

2. Propositional modal logic.

3. Possible worlds semantics.

4. Correspondence Theorem, modal definability.

5. Systems of modal logics.

6. Extension of modal logic: Hennessy-Milner modal logic.

7. Applications in CS, programming language semantics.

8. Basic ideas of $\mu$-calculus.

9. Temporal operators.

10. Temporal logic semantics.

11. Symbolic Model Checking.

12. Other extensions of classical logic.

13. Basic ideas of type theory.

14. Spare lecture.

Syllabus of tutorials:

1. Possibilities of classical propositional and predicate logics.

2. Propositional modal logic.

3. Possible worlds semantics.

4. Correspondence Theorem, modal definability.

5. Systems of modal logics.

6. Extension of modal logic: Hennessy-Milner modal logic.

7. Applications in CS, programming language semantics.

8. Basic ideas of $\mu$-calculus.

9. Temporal operators.

10. Temporal logic semantics.

11. Symbolic Model Checking.

12. Other extensions of classical logic.

13. Basic ideas of type theory.

14. Spare lecture.

Study Objective:

Study materials:

1. Colin Stirling: Modal and Temporal Preperties of Processes. Springer, 2001

2. Dirk van Dalen: Logic and Structure. Springer, 1980.

Note:

Further information:

No time-table has been prepared for this course

The course is a part of the following study plans:

• Computer Technology - Software Engineering- structured studies (compulsory elective course, compulsory elective course, S3 recommendation)
• Computer Technology - System Programming- structured studies (compulsory elective course)
• Computer Technology - Computer Graphics- structured studies (compulsory elective course)
• Computer Technology - Computer Network and Internet- structured studies (compulsory elective course)
• Computer Technology - Designing Digital Systems- structured studies (compulsory elective course)