Deciding logical properties of statements and its complexity

elective monographs

Foundations of mathematics 1000-211bPM
Languages, automata and computations 1000-214bJAO

Computational complexity 1000-218bZO
Logics for computer scientists 1000-217bLOG

Classroom

The lecture presents the state-of-the art knowledge concerning the way a dictionary of symbols one can construct statements from (i.e. quantifiers, connectives, relations and function symbols) impacts the complexity of the satisfiability and provability problems.

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

* 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.

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

* Homework 30%, exam 70%

* For PhD students: research homework 50%, exam 50%