Laboratorium z systemu
Coq 2009
System Coq wraz z dokumentacja dostepny jest pod adresem http://coq.inria.fr
1.
Zapoznanie sie z systemem, podstawowe komendy, taktyki...
wreczalt
cwiczenia1
przykladowe rozwiazania
cdn...
2.
Wstep do definicji indukcyjnych
wreczalt
cwiczenia2
cwiczenia3
3.
Definicje indukcyjne (c.d.)
match i fixpoint
drzewa
cwiczenia4
4.
Definicje indukcyjne - dowodzenie przez
indukcje
cwiczenia5
5.
Szachownica
cwiczenia6
szachownica rozwiazana
6.Zadania rozne
dziwna indukcja
zadania o le
problem Frobeniusa dla 3 i 5
funkcja Fibonaciego
funkcja Ackermanna
dobre ufundowanie
7. Selection sort - zadanie na uzycie taktyki Program
selection sort
8. Zadanie zaliczeniowe: jezyk slow w ktorych liczba a jest rowna
liczbie b
zadanie zaliczeniowe
Paradoksy i impredykatywnosc Set