Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (02.01.2024)
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.
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (02.01.2024)
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.
Podmínky zakončení předmětu
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
Předmět je zakončen ústní zkouškou.
Literatura -
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (07.12.2022)
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: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (07.12.2022)
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)
Požadavky ke zkoušce -
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
Požadavky budou upřesněny.
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
Will be specified later.
Sylabus -
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (07.12.2022)
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).