Budapesti Műszaki és Gazdaságtudományi Egyetem
Természettudományi Kar		 Tantárgy Adatlap
Tantárgy kód BMETE91AM58
Tantárgy azonosító adatok
1. A tárgy címe Bizonyításelmélet és a Coq programcsomag
2. A tárgy angol címe Proof Theory and Coq Proof Management System
3. Heti óraszámok (ea + gy + lab) és a félévvégi követelmény típusa 2 + 0 + 0 f Kredit 3
4. Ajánlott/kötelező előtanulmányi rend
vagy Tantárgy kód 1 Rövid cím 1 Tantárgy kód 2 Rövid cím 2 Tantárgy kód 3 Rövid cím 3
4.1
4.2
4.3
5. Kizáró tantárgyak
6. A tantárgy felelős tanszéke Algebra Tanszék
7. A tantárgy felelős oktatója Molnár Zoltán Gábor beosztása tanársegéd
Akkreditációs adatok
8. Akkreditációra benyújtás időpontja 2021.01.19 Akkreditációs bizottság döntési időpontja 2021.01.20.
Tematika
9. A tantárgy az alábbi témakörök ismeretére épít
Bevezető analízis, matematika alapjai.
10. A tantárgy szerepe a képzés céljának megvalósításában (szak, kötelező, kötelezően választható, szabadon választható)
Szabadon választható tárgy
11. A tárgy részletes tematikája

Induktív adattípusok, természetes számok, listák, fák és rekurziómentes adattípusok definiálása és manipulálása. Állítástípusok és bizonyítások definiálása és kezelése. A funkcionális programozás és a logika kapcsolata: Curry–Howard-izomorfizmus. A bizonyításkeresés automatizálása és elemi taktikák. A Coq teljes kifejezőereje: függő típusok és magasabb rendű logikák. Matematikai elméletek építése, modulok és taktikák programozása. 
12. Követelmények, az osztályzat (aláírás) kialakításának módja
szorgalmi
időszakban		 A félév során két zh, és prezentáció tartása vagy projektmunka bemutatása. vizsga-
időszakban
13. Pótlási lehetőségek
TVSZ szerint
14. Konzultációs lehetőségek
Megbeszélés szerint
15. Jegyzet, tankönyv, felhasználható irodalom
Yves Bertot, Pierre Casteran, 2004. Interactive Theorem Proving and Program Development: Coq Art, Springer.
16. A tantárgy elvégzéséhez átlagosan szükséges tanulmányi munka mennyisége órákban (a teljes szemeszterre számítva)
16.1 Kontakt óra
28
16.2 Félévközi felkészülés órákra
26
16.3 Felkészülés zárthelyire
16
16.4 Zárthelyik megírása
4
16.5 Házi feladat elkészítése
0
16.6 Kijelölt írásos tananyag elsajátítása (beszámoló)
16
16.7 Egyéb elfoglaltság
0
16.8 Vizsgafelkészülés
0
16.9 Összesen
90
17. Ellenőrző adat Kredit * 30
90
A tárgy tematikáját kidolgozta
18. Név beosztás Munkahely (tanszék, kutatóintézet, stb.)
Dr. Nagy P. Gábor
egyetemi tanár
Algebra Tanszék
Molnár Zoltán Gábor
tanársegéd
Algebra Tanszék
A tanszékvezető
19. Neve aláírása
Dr. Nagy P. Gábor