Proseminář z formálních důkazových metod - NMAL160

• Anglický název: Proseminar on formal proof methods
• Zajišťuje: Katedra algebry (32-KA)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2025
• Semestr: letní
• E-Kredity: 2
• Rozsah, examinace: letní s.:0/2, Z [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Garant: doc. Mgr. Štěpán Holub, Ph.D.
• Vyučující: doc. Mgr. Štěpán Holub, Ph.D.
• Třída: 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

Anotace

čeština

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.

Poslední úprava: Holub Štěpán, doc. Mgr., Ph.D. (29.05.2025)

angličtina

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

Poslední úprava: Holub Štěpán, doc. Mgr., Ph.D. (29.05.2025)