Deciding logical properties of statements and its complexity 1000-2M23ZWL
The course presents the knowledge concerning the relationship between the complexity and undecidability of satisfiability and provability problems for fragments of classical and intuitionistic logic. A proof of the property of interest for an example fragment of logic will be presented at each of the lectures. Then a discussion will follow on how to adapt the proof to other cases. The goal of the lecture is rather to show the critical mechanisms that emerge when an attempt to determine the property of the statement is made than to arrive at a table of complexities for fragments of logic.
1. The syntax of logical systems
2. The semantics of logical systems
3. The puzzle problem and its variants
4. The complexity in classical propositional calculus
5. The complexity in intuitionistic propositional calculus
6. Undecidable classes in classical logic without equality and function symbols
7. Decidable classes in classical logic without equality and function symbols
8. Undecidable classes in intuitionistic logic without equality and function symbols
9. Decidable classes in intuitionistic logic without equality and function symbols
10. Undecidable classes in classical logic with equality and function symbols
11. Decidable classes in classical logic with equality and function symbols, the finite model property case
12. Decidable classes in classical logic with equality and function symbols, with infinite models
13. Intuitionistic logic with function symbols and equality
Type of course
Mode
Requirements
Prerequisites
Course coordinators
Learning outcomes
Knowledge
K_W01 has in-depth knowledge of the branches of mathematics necessary to study computer science (logic and its connections with computer science, complexity theory)
K_W02 has in-depth understanding of the role and significance of the construction of mathematical reasoning
Abilities
K_U01 construct mathematical reasonings
K_U02 express computational problems in the language of mathematics
K_U04 design algorithms in basic computability models: Turing machines, logical circuits
K_U05 identify, for selected problems, if they belong to one of important complexity classes and if they are hard for them, using different characterizations of these classes
K_U07 analyse notions formalized in selected logical systems of computational significance, construct, with their help, formalizations of given notions or prove that such a formalization is impossible
K_U10 plan and realize personal lifelong education goals and stimulate and direct other people in doing so
K_U12 formulate and test hypotheses related to simple research problems
Social competences
K_K01 critically evaluate acquired knowledge and information
K_K02 recognize the significance of knowledge in solving cognitive and practical problems and the importance of consulting experts when difficulties arise in finding a self-devised solution
K_K03 think and act in an entrepreneurial way
Assessment criteria
* Homework 30%, exam 70%
* For PhD students: research homework 50%, exam 50%
Bibliography
* Egon Börger, Erich Grädel, Yuri Gurevich: The Classical Decision Problem. Perspectives in Mathematical Logic, Springer 1997
* M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149. Elsevier, 2006.
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
- Master's degree, second cycle programme, Mathematics
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: