Proseminar on formal proof methods - NMAL160

• Title: Proseminář z formálních důkazových metod
• Form of teaching: proseminar
• Guaranteed by: Department of Algebra (32-KA)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2025
• Duration in semesters: 1
• Semester: summer
• E-Credits: 2
• Hours per week, examination: summer s.:0/2, C [HT]
• Capacity: unlimited
• Maximum number of enrolled students: unlimited
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: taught
• Language: Czech
• Teaching methods: full-time
• Repeated enrollment: 2 / 2 / 2 / 2
• Guarantor: doc. Mgr. Štěpán Holub, Ph.D. et Ph.D.
• Teacher(s): doc. Mgr. Štěpán Holub, Ph.D. et Ph.D.
• Class: M Bc. MMIT > Doporučené volitelné; M Bc. MMIT > 1. ročník; M Bc. OM > Doporučené volitelné; M Bc. OM > 1. ročník

Annotation

English

An elective seminar on formal aspects of proofs, and on their computer verification.

Last update: Holub Štěpán, doc. Mgr., Ph.D. et Ph.D. (29.05.2025)

Czech

Volitelný proseminář je věnován rozboru důkazových postupů používaných v matematice (a tedy i v ostatních přednáškách), a to s ohledem na jejich formální přesnost. Kritériem přesnosti bude mechanická ověřitelnost počítačem (bude používán důkazový asistent Isabelle). Proseminář je proto také úvodem do tématu počítačové verifikace matematiky.

Last update: Holub Štěpán, doc. Mgr., Ph.D. et Ph.D. (29.05.2025)