# KIT Course: Constructive Logic (So'24)

Constructive Logic (Summer 2024)
Instructor: André Platzer
Teaching
Assistants:
Enguerrand Prebet, tik@teberp.dnarreugne
ECTS: 5 (3+1 SWS)
Semester: Summer 2024
Time:
 Mon 11:30-13:00 in 50.34 room 131 Thu 09:45-11:15 in 50.34 room 131
This course counts toward the Vertiefungsfach Theoretische Grundlagen or the Vertiefungsfach Softwaretechnik / Übersetzerbau or the Wahlbereich Informatik in the KIT Master of Science in Informatics curriculum.
Questions
Schedule
DESCRIPTION:

This course provides a thorough introduction to modern constructive logic, emphasizing its numerous applications in computer science, and its mathematical properties. The core topics of this course are intuitionistic logic, natural deduction, Curry-Howard isomorphism, propositions as types, proofs as programs, formulas as programs, constructive logic as functional programming, constructive logic as logic programming, Heyting arithmetic induction as primitive recursion, cut elimination, sequent calculus, contraction-free proofs, inversion, and decidable fragments. Advanced topics may include type theory, proof search, linear logic, temporal logic, intuitionistic modal logic.

Students who successfully complete this course will:

• Understand the working principles of logic
• Understand how the meaning of a proposition comes from its verifications
• Distinguish propositions from judgments
• Use proof rules to conduct formal proofs
• Justify how proof rules fit to one another in sound and complete ways
• Assess the validity of a formal proof
• Understand propositions as types, proofs as programs, formulas as programs
• Relate constructive logic to computation and constructive proofs to functional programs
• Relate deductive proof search to computation in logic programming
• Relate induction to recursion and use induction to prove properties in and about logical systems
• Understand the principles and applications of logic programming

METHOD OF EVALUATION:
Grading will be based on a final exam. Final exam: Wed 25.9. Closed book, one double-sided sheet of hand-written notes permitted. Also see exams from prior semesters.