Formal Mathematics and Proof Assistants - NMMB568

• Anglický název: Formal Mathematics and Proof Assistants
• Zajišťuje: Katedra algebry (32-KA)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2024
• Semestr: letní
• E-Kredity: 4
• Rozsah, examinace: letní s.:2/1, Z+Zk [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: angličtina
• Způsob výuky: prezenční
• Garant: Mgr. Josef Urban, Ph.D.; RNDr. Martin Suda, Ph.D.
• Vyučující: RNDr. Martin Suda, Ph.D.; Mgr. Josef Urban, Ph.D.
• Třída: M Mgr. MMIB; M Mgr. MMIB > Volitelné
• Kategorizace předmětu: Matematika > Algebra
• Neslučitelnost : NMMB566
• Záměnnost : NMMB566
• Je neslučitelnost pro: NMMB566
• Je záměnnost pro: NMMB566

Anotace

čeština

The topic of the course are formal (computer-understandable) mathematics and proof assistants (interactive theorem provers). A proof assistent is a tool to assist with the development of formal proofs by human-machine collaboration. The language of communication is some variant of formal logic and the main aim a high level of assurance that the proven actually holds.We will have a look at the proof assistent Lean, study its theoretical foundations and explore the ways in which it can be used to develop theories, model systems, and prove theorems in computer science as well as mathematics.

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

Podmínky zakončení předmětu

Předmět je zakončen ústní zkouškou.

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

Literatura

čeština

Blanchette et at. The Hitchhiker's Guide to Logical Verification (available online)

Jeremy Avigad, Leonardo de Moura, and Soonho Kong. Theorem Proving in Lean (available online)

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

Požadavky ke zkoušce

čeština

Požadavky budou upřesněny.

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

angličtina

Will be specified later.

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

Sylabus

čeština

Většinou se budeme řídit textem The Hitchhiker's Guide to Logical Verification:

Základy:

• definice a výroky,

• Backward Proofs, Forward Proofs,

(kvantifikátory, spojky, taktiky, věty jako typy / důkazy jako termy).

Funkcionálně-logické programování:

• funkcionální programování,

• induktivní predikáty,

• monády,

(základní datové struktury, důkazy indukcí, aritmetické taktiky).

Sémantika programů:

• operační sémantika,

• Hoareova logika,

• denotační sémantika,

(small-step/big-step, částečná vs. úplná správnost, monotónní funkce, svazy a pevné body).

Matematika:

• logické základy matematiky,

• základní matematické struktury,

• racionální a reálná čísla,

(základní principy, podtypy, kvocientové typy, třídy typů).

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

angličtina

We will mostly follow the Hitchhiker's Guide:

Basics:

• Definitions and Statements,

• Backward Proofs, Forward Proofs

(Quantifiers, Connectives, Tactics, Propositions as Types / Proofs as Terms)

Functional–Logic Programming:

• Functional Programming

• Inductive Predicates

• Monads

(Basic Data Structures, Proofs by induction, Arithmetic tactics)

Program Semantics:

• Operational Semantics

• Hoare Logic

• Denotational Semantics

(Small-step/big-step, Partial vs Total correctness, Monotone functions, lattices and

fixpoints)

Mathematics:

• Logical Foundations of Mathematics

• Basic Mathematical Structures

• Rationals and Real Numbers

(Foundational principles, Subtypes, Quotient types, Type Classes)

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)