Jakob-Haringer-Str. 2

5020 Salzburg, Austria

Room 2.17


+43 (0)662 8044 6417

+43 (0)662 8044 611 (fax)

Skype ana_sokolova

Many thanks to Silviu Craciunas for the photo (RTAS 2010 in Stockholm) and his help with iWeb!

Formale Systeme 511.001 (lectures), Winter semester 2019/2020

Schedule:            Wednesdays 2pm-3pm / from 9.12.19 Mondays 2pm-3pm

                            Thursdays 10am-12am

                            starting 3.10.2019 in T01 see calendar

First meeting:       Thursday, October 3 at 10am in T01

Language:           Teaching in German, course material (mainly) in English

Office hours:       Wednesdays 11am-12am 

Tutorium:            Tuesdays 4pm-6pm in T01


  1. Textbook: Logical Reasoning: A First Course, by Rob Nederpelt and Fairouz Kameraddine, King’s College London Publications, 2007. [LR]

  1. Textbook: How to Think Like a Mathematician, by Kevin Houston, Cambridge University Press, 2009. [Think]

  2. Lecture Notes on Math Basics by Harald Woracek, TU Vienna, 2017 [LN]

  1. Textbook: Modellierung: Grundlagen und formale Methoden by Uwe Kastens and Hans Kleine Buening, Hanser, 2005. [Mod]

  1. Textbook: Introduction to Automata Theory, Languages, and Computation by John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman, Pearson/Addison-Wesley, 2007. [Aut]

  2. Textbook: Introduction to the Theory of Computation, by Michael Sipser, Cengage, 2005. [Comp]

The books can be ordered via . Some copies are available at the department library.

Prerequisites:  None, the course material is self-contained, as are the textbooks.

Exam:   The exam is written. In case a student wants to improve his/her grade, an additional oral exam can be scheduled. One can pass the exam by either (1) passing the two partial tests within the semester, or (2) passing one of the possible full exams that will be scheduled after the semester ends. The tests/exam consist of several exercises from the material covered during the course.

In order to pass via the partial tests (1) one needs to: have in sum a total of 55% of the maximal points available at both tests and no less than 20% of the maximal number of points at each one test. That is, if partial test 1 brings maximally 100 points and partial test 2 also 100 points, in order to pass one needs to have at least 20 points on each test and a total sum of at least 110 points on both tests.

In order to pass via one of the exam possibilities one needs to have 55% of the maximal points available at the exam. That is, if the exam brings maximally 100 points, in order to pass one needs to have at least 55 points.

Note that the exams cover the full course material, whereas each partial test covers one half of the material.

Exam dates: The first feedback test will take place on Friday December 13 in T01 and HS2 at 2pm.

                      On Friday December 6 from 1pm to 3pm in HS2 we will have a Q&A session -- an extra class as preparation for the test.

                      Here is an example set of tasks, to be discussed on December 6.


                      The second feedback test will take place on Monday February 3 in HS01 and HS02 at 2pm.

                      On Friday January 31 from 1pm to 3pm in HS2 we will have a Q&A session -- an extra class as preparation for the test.

                      Here is an example set of tasks, to be discussed on January 30.

                      The first exam possibility is on Monday Febrary 17 in T01 at 2pm.

                      Please register for the first exam possibility via PlusOnline.

Course description:  This is a first-semester obligatory course on basics of theoretical computer science: logic and sets.

In this course we will learn the basics of formal methods, the alphabet :-) necessary to read and write basic theoretical computer science. In particular we will learn logic and logical reasoning (propositional and predicate logic, basic proof methods) and apply it to learn and understand sets, relations, functions, orderings, algebra, finite automata, labelled transition systems, and Hoare triples for reasoning about programs.

Slides:  Whenever slides are used, they will be made available on this webpage. The slides are by no means complete and only serve as help for better presentation. More material is covered during the class (on the blackboard) than visible on the slides.


  1. Week 1, Thursday 3.10.19, Introduction and Puzzles, first meeting. At the end of the slides, I gave you some puzzles to solve. The puzzle sets are part of the slides, feel free to continue solving more. The point of the puzzles is that they illustrate several important concepts of theoretical computer science, and also show you the need of abstraction, formal reasoning, and the ability to communicate the solutions. We briefly discuss couple of this puzzles next week.
    Here are the slides.

  2. Week 2, Wednesday 9.10.19 and Thursday 10.10.19, Sets and we will start with propositional logic. Here are the slides: sets-slides and propositional-logic-slides, also with all stages of build: sets-slides-all-stages and propositional-logic-slides-all-stages. We finished the discussion on Sets, I will send you the lecture notes per email, and we also started with Propositional Logic, including slide 7. Please read the lecture notes that I have sent you as well as Chapter 1 and Chapter 2 from [LR].

  3. Week 3, Wednesday 16.10.19 and Thursday 17.10.19, we continued with propositional logic: truth tables, truth functions, equivalence of propositions, standard equivalences - until slide 48 from the propositional-logic slides. Please read Chapter 3,4, and 5 from [LR].

  4. Week 4, Wednesday 23.10.19 and Thursday 24.10.19: Calculating with propositions, strengthening and weakening, calculating with weakenings - until the end of the propositional-logic slides. Please read Chapter 6 and 7 from [LR].

  5. No class in week 5 due to public holidays and my traveling. As preparation for week 6 (in case you wish to print the slides in advance), here are the predicates-and-quantifiers-slides, also with all stages of build predicates-and-quantifiers-slides-all-stages.

  6. Week 6, Wednesday 6.11.19 and Thursday 7.11.19: Predicates and quantifiers, equivalences with quantifiers. We covered the material up to (including) slide 15 from the predicates-and-quantifiers slides. Next week we will give more examples and calculate with predicate formulas. Please read Chapter 8 and Chapter 9 up to (including) Section 9.5 from [LR].

  7. Week 7, Wednesday 13.11.19 and Thursday 14.11.19: Calculating with predicate formulas; Derivations (in particular derivation rules for conjunction and implication). We covered the rest of the material shown in the predicates-and-quantifiers slides, and until (including) slide 10 of the derivation-slides. Here are also the derivation slides with all stages of build. Please read the rest of Chapter 9 (also read Chapter 10 which we did not discuss in class much), and Chapter 11, 12, and 13 from [LR].

  8. Week 8, Wednesday 20.11.19 and Thursday 21.11.19: Reasoning with other connectives; reasoning (derivations) with predicates and quantifiers -- only the alternative rules for existential quantification remain for next week. We covered the material summarized until (including) slide 32 in the derivation slides. Please read Chapter 14 and Chapter 15 until Section 15.3 from [LR].

  9. Week 9, Wednesday 27.11.19 and Thursday 28.11.19: Alternative rules for existential quantification. We finished the material summarized in the derivation slides. Please read the rest of Chapter 15 from [LR]. Then we discussed relations, special types of relations. Please read Chapter 17 from [LR] -- you may also wish to read Chapter 16 as preparation, if you have not done so before. Here are the relation-slides, of which we covered the material summarized up to (including) slide 9. Here are also the relation slides with all stages of build. In addition, I will send you lecture notes on relations via email by next week.

  10. Week 10, Wednesday 4.12.19 and Thursday 5.12.19: We continued with relations: equivalences, equivalence classes, partitions, the correspondence theorem, transitive closure. Please read the rest of Chapter 17 (from Section 17.5) from [LR], and again I will send you my lecture notes via email. We are done with the relation-slides. Next week we will discuss functions --- here are the function-slides in advance, and here are the function slides with all stages of build.

  11. Week 11, Monday 9.12.19 and Thursday 12.12.19: Functions, surjections, injections, bijections, operations on functions -- characterisations, properties, and examples. Please read Chapter 18 from [LR], and again I will send you my lecture notes via email. We are done with the function-slides, but we will still prove some of the properties next week. Next week we will also discuss structures, numbers, cardinals --- here are the naturals-and-cardinals-slides in advance, and here are the naturals-and-cardinals-slides with all stages of build.

  12. Week 12, Monday 16.12.19 and Thursday 19.12.19: The structure of natural numbers, induction, cardinals.  We will still prove some properties about cardinals next time, in January. Please read Chapter 19 from [LR] and I will send you my lecture notes via email. Happy Holidays!

  13. Week 13, Wednesday 8.1.20 (extra class - 2 hours, 1pm-3pm, catching up) and Thursday 9.1.20 -- Happy New Year!: We had fun proving some of the properties related to cardinals; and started with a new topic: Automata. Here are the automata slides, and here the automata slides with all stages of build. So far we focused on DFA only, and cover the material up to (including) slide 6. You may read on deterministic finite automata from any source, e.g., the books by Sipser [Comp] Section 1.1, or Hopcroft et al [Aut] Section 2.1 and 2.2. I strongly recommend reading the very nice introduction (Chapter 0) in [Comp], or the introductory Chapter 1 of [Aut], in particular Section 1.5. In addition, I will send you my lecture notes via email.

  14. Week 14, we will only have a class on Monday 13.1.20 -- no classes on Thursday due to my travelling. However, on Thursday 10-12 there will be a tutorial class in T01 in which the tutors will discuss algebraic structures with you, a topic that we do not cover in class. Here are the lecture notes on algrebraic structures that you are expected to read and get familiar with for future courses (e.g. this knowledge may be expected from you in Discrete Mathematics).

  15. Week 15, Monday 20.1.20 and Thursday 23.1.20: Automata, continued. We proved some of  the closure properties and motivated the study of nondeterminism. We then continued with nondeterministc finite automata (NFA) and equivalence of NFA and DFA (the powerset construction). We covered the material up to slide 13 from the automata slides. You may read Section 1.2 and 1.3 from [Comp] or 2.3-2.5 and 3.1 and 3.2 from [Aut]. I will also send you my notes via email.

  16. Week 16 -- no class on Monday 27.1.20, due to my traveling, but normal classes on Thursday 30.1.20 and an extra class (Q&A) session on Friday 31.1.20 (see above section on exams!). There will also be an extra tutorial on Friday 31.1.20 for several hours after the Q&A session. We further proved the closure properties, and discussed nonregularity of languages and the pumping lemma. You may read Section 1.4 from [Comp] and few sections in Chapter 3 and 4 of [Aut].

Ana Sokolova

Dr. TU Eindhoven, The Netherlands, 2005

Associate Professor

Computational Systems Group

Department of Computer Sciences

University of Salzburg