Cvičení VPL, 2019/20, Ct 9:00 S8

V záznamníku učitele (v SISu) jsem k vašemu jménu u tohoto cvičení vložil pseudonáhodný pseudokód.
Podle něho se najděte.

Oznamy:
DU3 programatorska do 6.11.

Inicialy/Pseudojmena		3.10.	10.10	10.10	17.10	31.10	7.11	28.11	5.12.	12.12
				(DU1)	DU2	DU3(10b)DU4	DU5	DU6	DU7	DU8	DU9	SUM9 ZAP(9.1.)	

			A	2	4	10-	4,5						20,5
			B	.	.
			C	2*	2	9	3m	4m*					20	7P
			D	4-	5-	10	5	5m*		5		5	39	ZAP
			E	1	5-	10*	(2j)						18
				-
			F	.	.
			G	3	.	10*	5m						(18)	ZAP
			H	.	4,9	10	5-*	5-	4		4-	5	37,9	ZAP
			I	5	3		5	5m*	4m	1	1	4,5	28,5	3P
			J	.	4,9	10		5m*	2m	3m	1m	5	30,9	2P
				-
			K	3	4	10	3	5m*	0m	1m	5*	5	36	ZAP
			L	4,5	5	10	5	5	4,5		3	5	42	ZAP
			M	.	.
			N	.	5	10	5	5		2	2	5	34	ZAP
			O	3	4		3	4m*	0m				14
				-
			P	.	4,9	10	5	4		4		5	32,9	1P
			Q	.	.
			R	.	.
--			------------------------------------------------------------------------------------------
Pocet				9	12+1	10	10+1	10*	6	6	6	8


Body za kazdou ulohu: 0-5, vyjimka DU3: 10 b, celkem 50b
Pozadavek na zapocet: 33,3 z 50b (2/3 bodů)
(defaultni datum v SIS: ..Ct 9.1.2020)
Náhradní příklady: 1 příklad za 2 (chybějící) body. (Budou na stránkách)


(*) opraveno dodatecne

DU1 3.10. Prevod Bipartitni graf na SAT
DU2 10.10. Prevod Neekvispaced posloupnosti na SAT
DU3 10.10 na 6.11. Programatorsky, podle DU2
DU4 17.10. Tablem dokazte: PG2018.4.4c 
DU5 31.10. Dokažte rezolucí: PG2019/5.6
DU6  7.11. Dokažte nebo vyvraťte (sémanticky z def.) PG2018/6.9
--  14.11. neni DU
--  21.11. neni cviceni
DU7 28.11. Tranzitivita rovnosti, tablem (PG2019/10.6b)
DU8  5.12. Definujte formuli jednoprvkove mnoziny; PG2019/8.8c
DU9 12.12. Prevedte na formuli nerozsireneho jazyka: PG2019/11/6c
DU10 19.12. není



------------
Priklady 2018: (+zadano)
DC1. 1.10. Bipartitní graf
DC2. 15.10. Převod na DNF,CNF a modely (pr 2.12)
DC3. 22.10. Popiste vsechny (nekonecne) modely
DC4. 29.10. Dokazte tablo metodou: (p->(q->r))->((p->q)->(p->r))
DU5. 19.11. Definovatelnost nejvys jednoprvkovych mnozin
DU6. 26.11. Tablo pro PL
DU7. 10.12. Gr:9.7b Tranzitivita rovnosti.
DU8. 17.12(posledni) Gr:11.11d Prevod a skolemizace


Priklady 2017: (+zadano)
DC1.  4.10. Bipartitni graf
DC2. 11.10. Jednotkova propagace
DC3. 18.10. Tablo-dukaz pro formuli x^(yvz) -> (x^y)v(x^z)
-    25.10.
-     1.11
P1 1) Graf, 2) Tablo-dukaz, 3) rezoluce, 4) pro teorii najdete
DC4  29.11. Mame F=(forall x)(exists y) f(x,y) a G=(exists y)(forall x) f(x,y)
	Dokazte anebo vyvratte F->G a G->F
DC5  13.12. 10.6.a) Převeďte do prenexního tvaru:
	(forall y)((exists x)P(x,y) -> Q(y,z)) ^ (exists y)((forall x)R(x,y) v Q(x,y)) 
P2 1) Tablo, 2) Prenexni tvar a skolemizace, 3) Rezolventy a unifikace


zadano 2016/17
1. 18/10 VF do CNF a DNF
2. 25/10 2/2a
3.  1/11->29/11 tablo VL: tranzitivita ekvivalence
4. 29/11 9/3a 
5.  6/12 9/5b tranzitivita "=" pomoci tabla
6. 13/12 9/9c prenexni tvar
7. 20/12 10/3 Veta o dedukci transformaci tabel


  Nahradni priklady 2016, kazdy za (max.) 2 body 
10/1a Tablo pro symetrii rovnosti
10/6b+7b prenexni+skolemizace
 9/3i tablo pro kvantifikatorovou upravu