Laboratorium z systemu Coq                            

1. Zapoznanie sie z systemem, podstawowe komendy, taktyki...

wreczalt         cwiczenia1         przykladowe rozwiazania
 
 

2. Wstep do definicji indukcyjnych

3. Definicje indukcyjne (c.d.)

4. Definicje indukcyjne - operator punktu stalego i dowodzenie przez indukcje

5. Zaawansowane taktyki dla typow indukcyjnych Discriminate, Injection, Inversion.

6. Modelowanie rachunku procesow.

7. Szachownica

Zadania z ubiegłych lat

0. Intuicjonistyczna logika zdaniowa

1. Intuicjonistyczna logika zdaniowa (ciag dalszy)

2. Porównanie arytmetyki Heytinga i arytmetyki Peano pierwszego rzedu

3. Drzewa AVL

4. Porzadki dobrze ufundowane