Deciding logical properties of statements and its complexity
General data
Course ID:  10002M23ZWL 
Erasmus code / ISCED: 
11.3

Course title:  Deciding logical properties of statements and its complexity 
Name in Polish:  Złożoność określania własności logicznych stwierdzeń 
Organizational unit:  Faculty of Mathematics, Informatics, and Mechanics 
Course groups: 
Elective courses for 2nd stage studies in Mathematics Elective courses for Computer Science 
ECTS credit allocation (and other scores): 
6.00

Language:  English 
Type of course:  elective monographs 
Requirements:  Foundations of mathematics 1000211bPM 
Prerequisites:  Computational complexity 1000218bZO 
Mode:  Classroom 
Short description: 
The lecture presents the stateofthe 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. 
Full description: 
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 
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 CurryHoward Isomorphism, volume 149. Elsevier, 2006. 
Learning outcomes: 
Knowledge K_W01 has indepth knowledge of the branches of mathematics necessary to study computer science (logic and its connections with computer science, complexity theory) K_W02 has indepth 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 selfdevised solution K_K03 think and act in an entrepreneurial way 
Assessment methods and assessment criteria: 
* Homework 30%, exam 70% * For PhD students: research homework 50%, exam 50% 
Classes in period "Summer semester 2023/24" (past)
Time span:  20240219  20240616 
Navigate to timetable
MO TU W TH FR WYK
CW

Type of class: 
Classes, 30 hours
Lecture, 30 hours


Coordinators:  Aleksy Schubert  
Group instructors:  Aleksy Schubert  
Students list:  (inaccessible to you)  
Examination:  Examination 
Copyright by University of Warsaw.