Poll

No polls currently selected on this page!

Repository

Repository is empty

Mathematical logic in computer science

Code: 61527
ECTS: 5.0
Lecturers in charge: prof. dr. sc. Mladen Vuković - Lectures
Lecturers: prof. dr. sc. Mladen Vuković - Exercises
English level:

1,0,0

All teaching activities will be held in Croatian. However, foreign students in mixed groups will have the opportunity to attend additional office hours with the lecturer and teaching assistants in English to help master the course materials. Additionally, the lecturer will refer foreign students to the corresponding literature in English, as well as give them the possibility of taking the associated exams in English.
Load:

1. komponenta

Lecture typeTotal
Lectures 30
Exercises 15
* Load is given in academic hour (1 academic hour = 45 minutes)
Description:
COURSE AIMS AND OBJECTIVES: Insight into some aspects of mathematical logic contributing directly to current software technology.

COURSE DESCRIPTION AND SYLLABUS:
1. Proving in propositional and predicate calculi. Resolution and decision diagrams for the propositional calculus. Resolution for the predicate calculus. Herbrand's theorem. SLD-resolution and logic programming, Prolog. Validity tests (semantic tableaux).
2. Temporal logic and model checking. Temporal formulae and their semantics. Kripke models and transition systems. Fairness, safety and liveness in distributed systems. Validity tests for LTL. Expressivity of LTL. Other models of time: CTL, CTL*. Model checking algorithms for LTL and CTL*. State abstraction and symbolic model checking. Model checking in software development - algorithms and tools.
3. Other modal logics in computer science. The logics of actions and programs, dynamic logic. Hoare's triples and program verification. The logics of knowledge and belief. Distributed and common knowledge. Modelling and verification with KT45n.
TEACHING AND ASSESSMENT METHODS:
Students' obligations during classes: Lecture and tutorial attendance, elaboration of homework, passing 2 mid-term exams.
Signature requirements: Attendance at 70% of lectures and tutorials, submission of results for 70% of homework, passing grade at all mid-term exams.
Taking of exams: Final examination is taken either in written or oral form. Final grade is based on successful elaboration of homework, grades for mid-term exams and final examination grade.
Literature:
  1. M. Ben-Ari: Mathematical Logic for Computer Science
  2. M. Huth, M. Ryan: Logic in Computer Science
  3. E. M. Clarke, O. Grumberg, D. A. Peled: Model-Checking
  4. Z. Manna, A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems
  5. R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi: Reasoning about Knowledge
  6. P. Blackburn, M. de Riejke, Y. de Venema: Modal Logic
  7. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen: Systems and Software Verification
  8. M. Vuković: Matematička logika
3. semester
Izborni predmet 3, 4, 5, 6 - Regular study - Computer Science and Mathematics

4. semester
Izborni predmet 3, 4, 5, 6 - Regular study - Computer Science and Mathematics
Consultations schedule: