Cvičení VPL, 2017/18, St 10:40 S7


Inicialy
	SUM 	1   2	3   P1   	    4	5   P2		SUM(36/55)
DB		.   4	2   17+(5,5,4,2+)	5   9(432)	37 ZAP
JD		.   5	5m			    8(440)	18
VK		.   5				   		 5
OK		.   5	5-  15-(5-,5,1,4)   4	5   10(442)	44 ZAP
MK		.   5	    12(4,1,5,2)     5-	2j  6(114)	30
AM		.   5-	4   14(4,5,4,1)     2*	5   9(432)	39 ZAP
MM		.   5	4   13(5,5,1,2)     3	4m  7(331)	36 ZAP
MP		.   5-	5			3		13
FR		.   5	5   17(4,5,5,3)		3   10(424)	40 ZAP
PR		.   5	5   16(4,5,4,3)     4	5   11(344)	46 ZAP
JŠ		.   5	5-  17-(4,5-,5,3)   1	4   11(542)	43 ZAP
RW		.   5	4   18(4,5,5,4)	    5-	4   11(533)	47 ZAP
Anonym                                      4b/mail

Body za kazdou ulohu: 0-5, celkem 55
Pozadavek na zapocet: 36 (2/3 bodů)
(defaultni datum v SIS: 16.1.2018)

(*) opravene dodatecne

Priklady: (+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


Náhradní příklady budou.


-------------------
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