Logic and computation theory 1000-2D08LTO
Traditionally, logic studied the laws of thought. Today, computers make it possible to process a big amount of information outside human mind. Not surprisingly, the development of computer science gives rise to new challenges for logic. Out of many fascinating possibilities, we have chosen the following topics.
Complexity theory. Complexity theory studies the resources needed to solve problems, resources such as time and memory, the number of processors, or maybe the number of random bits needed. The security of asymmetric cryptography is based on assumptions from computational complexity, even though these assumptions remain unproved. The connection between complexity theory and logic is a field called descriptive complexity, which shows that questions about the relationships between complexity classes (such as P, NP, PSPACE) can be rephrased as questions about the expressive power of different logics (usually fixpoint extensions of first-order logic).
Mathematical verification of hardware and software. Some computer systems are so important, that their correctness cannot be judged by mere testing; one needs more thorough methods. One of these methods is building a mathematical model of the system, and proving that this model has no incorrect behaviors. Commonly used models involve games, where an evil environment tries to steer the system into an incorrect state, and a controller tries to avoid this. Logic is used to precisely state what incorrect behaviors are, so that an automatic tool can search all behaviors of the model for incorrect ones. Logics used in verification include temporal and fixpoint logics, and the underlying technical tools are often finite automata.
Classical automata theory. Despite being one of the older fields in computer science, automata theory still offers unsolved, but simply stated problems. Consider the following, still open, question about regular expressions: is there a regular language that cannot be described by a regular expression (complementation is allowed) that has no nesting of the star operation? (The star is allowed, but inside a star there is no other star.) The seminar will study such questions, also for more general automata models, such as tree automata, or automata on infinite words.
Type of course
Learning outcomes
Knowledge
Student learns about research problems in the current studies in the area of logic in computer science. She or he should start her/his own supervised research, which will become the basis of her/his Master Thesis.
Skills
Student can
1. read scientific papers with understanding,
2. communicate scientific results to others in a clear and attractive way,
3. listen in an attentive manner and ask questions to speakers.
Competence
Students gets knowledge about research methodology in the area of logic in computer science. She or he gets a general knowledge about various publication venues and their scientific prestige.
Assessment criteria
The required condition is a careful preparation and presentation of at least one lecture during a semester, and---depending on the year of studies--the acceptance of a subject of the Master Thesis, or submission of the thesis itself.
Bibliography
Modern scientific literature of the subject, including scientific journals and data from Internet. Details are provided by the lecturers at the first meeting.
Additional information
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: