====== Státní závěrečná zkouška ======
===== Logika =====
^  A  ^  B  ^  ¬A  ^  ¬B  ^  A ∨ B  ^  A ∧ B  ^  A ⇒ B  ^  A ⇔ B  ^
|  F  |  F  |   T  |   T  |    F    |    F    |    T    |    T    |
|  F  |  T  |   T  |   F  |    T    |    F    |    T    |    F    |
|  T  |  F  |   F  |   T  |    T    |    F    |    F    |    F    |
|  T  |  T  |   F  |   F  |    T    |    T    |    T    |    T    |
==== Zákony výrokové logiky ====
^  #  ^  Název  ^  IN  ^  OUT  ^
|  1  |  Zákon ekvivalence  |  A ⇔ B  |  (A ⇒ B) ∧ (B ⇒ A)  |
|  2  |  Zákon implikace  |  A ⇒ B  |  ¬A ∨ B  |
|  3  |  Zákony komutativní  |  A ∨ B  |  B ∨ A  |
|:::|:::|  A ∧ B  |  B ∧ A  |
|  4  |  Zákony asociativní  |  A ∧ (B ∧ C)  |  (A ∧ B) ∧ C  |
|:::|:::|  A ∨ (B ∨ C)  |  (A ∨ B) ∨ C  |
|  5  |  Zákony distributivní  |  A ∨ (B ∧ C)  |  (A ∨ B) ∧ (A ∨ C)  |
|:::|:::|  A ∧ (B ∨ C)  |  (A ∧ B) ∨ (A ∧ C)  |
|  6  |  Zákony zjednodušení disjunkce  |  A ∨ T  |  T  |
|:::|:::|  A ∨ F  |  F  |
|:::|:::|  A ∨ A  |  A  |
|:::|:::|  A ∨ (A ∧ B)  |  A  |
|  7  |  Zákony zjednodušení konjunkce  |  A ∧ T  |  A  |
|:::|:::|  A ∧ F  |  F  |
|:::|:::|  A ∧ A  |  A  |
|:::|:::|  A ∧ (A ∨ B)  |  A  |
|  8  |  Zákon vyloučení třetího  |  A ∨ ¬A  |  T  |
|  9  |  Zákon sporu  |  ¬(A ∨ ¬A)  |  F  |
|  10  |  Zákon identity  |  A  |  A  |
|  11  |  Zákon negace  |  ¬(¬A)  |  A  |
|  12  |  Zákony De Morganovy  |  ¬(A ∧ B)  |  ¬A ∨ ¬B  |
|:::|:::|  ¬(A ∨ B)  |  ¬A ∧ ¬B  |
|  13  |  Eliminace AND  |  A<sub>1</sub> ∧ A<sub>2</sub> ∧ … ∧ A<sub>n</sub> ⇒ A<sub>i</sub>; i ∈ <1, n>  ||
|  14  |  Zavedení OR  |  A<sub>i</sub> ⇒ A<sub>1</sub> ∨ A<sub>2</sub> ∨ … ∨ A<sub>n</sub>; i ∈ <1, n>  ||
|  15  |  Přesun kvantifikátorů doleva (x se nevyskytuje v B!)  |  Qx(A) ∨ B  |  Qx(A ∨ B)  |
|:::|:::|  Qx(A) ∧ B  |  Qx(A ∧ B)  |
|  16  |  Přesun negace dovnitř  |  ¬(∀x(A))  |  ∃x(¬A)  |
|:::|:::|  ¬(∃x(A))  |  ∀x(¬A)  |
|  17  |  Distributivní zákon pro kvantifikátory  |  ∀x(A) ∧ ∀x(B)  |  ∀x(A ∧ B)  |
|:::|:::|  ∃x(A) ∨ ∃x(B)  |  ∃x(A ∨ B)  |
|  18  |  Přejmenování vázaných proměnných  |  ∀x(A(x)) ∨ ∀x(B(x))  |  ∀x∀y(A(x) ∨ B(y))  |
|:::|:::|  ∃x(A(x)) ∧ ∃x(B(x))  |  ∃x∃y(A(x) ∧ B(y))  |

==== Rezoluční metoda ====
Abychy mohl rezolvovat, musím:
  -Disjunktivní normální forma (//a ∨ b ∨ c ∨ d//)
  -Prenexní normální forma (přejmenovat, všechny kvantifikátory doleva, //∃x∀zQ(x,z)⇒∃x∃zQ(x,z) ⇔ ∃x∀zQ(x,z)⇒∃v∃wQ(v,w) ⇔ ∃x∀z∃v∃w(Q(x,z)⇒Q(v,w))//)
  -Skolemova normální forma (zbavení se ∃, proměnné nahazeny konstantami (funkcemi), //∃x∀z∃v(Q(x,z)⇒Q(v,x)) ⇔ ∀z∃v(Q(a,z)⇒Q(v,a)) ⇔ ∀z(Q(a,z)⇒Q(f(z),a))//)

=== Příklad ===
Z následující databáze
  *Kdo senučil, neumí rezoluční metodu.
  *Kdo umí rezoluční metodu, získá body.
  *Kdo získá body, složí zkoušku z IZU.
  *Někdo složí zkoušku z IZU, přestože se neučil.
dokažte pomocí rezoluční metody tvrzení:
  *Někdo složí zkoušku z IZU, přestože neumí rezoluční metodu.

----
  *∀x(¬učil(x) ⇒ ¬umí(x))
  *∀x(umí(x) ⇒ body(x))
  *∀x(body(x) ⇒ zkouška(x))
  *∃x(zkouška(x) ∧ ¬učil(x))

  *¬∃x(zkouška(x) ∧ ¬umí(x))

----
  *∀x(učil(x) ∨ ¬umí(x))
  *∀x(¬umí(x) ∨ body(x))
  *∀x(¬body(x) ∨ zkouška(x))
  *∃x(zkouška(x) ∧ ¬učil(x))

  *∀x(¬zkouška(x) ∨ umí(x))

----
  -{učil(x), ¬umí(x)}
  -{¬umí(x), body(x)}
  -{¬body(x), zkouška(x)}
  -{zkouška(a)}
  -{¬učil(a)}
  -{¬zkouška(x), umí(x)}

----
  *{umí(a)} //rezolventa z 6 a 4, [z/a]//
  *{učil(a)} //rezolventa z 7 a 1, [z/a]//
  ***{}**

===== Prolog =====
==== Zásobník ====
<code prolog>
push(E, T, [E|T]).  %vložení prvku

pop(E, [E|T], T).   %výběr prvku
</code>

==== Fronta ====
<code prolog>
enqueue(E, [], [E]).                               %vložení prvku
enqueue(E, [H|T2], [H|T3]) :- enqueue(E, T2, T3).

dequeue(E, [E|T], T).                              %výběr prvku
</code>

==== Fronta s prioritou ====
<code prolog>
insert(E, [], [E]).                                              %vložení prvku
insert(E, [H|T], [E, H|T]) :- precedes(E, H).
insert(E, [H|T2], [H|T3]) :- precedes(H, E), insert(E, T2, T3).

precedes(A, B) :- A < B.                                         %platí pouze pro čísla!

dequeue(E, [E|T], T).                                            %výběr prvku
</code>

==== Množina ====
<code prolog>
add(E, S, S) :- member(E, S), !.                                                 %vložení prvku
add(E, S, [E|S]).

delete(E, [], []).                                                               %výběr prvku
delete(E, [E|T], T) :- !.
delete(E, [H|T2], [H|T3]) :- delete(E, T2, T3).

intersection([], _, []).                                                         %průnik dvou množin
intersection([H|T1], S2, [H|T3]) :- member(H, S2), !, intersection(T1, S2, T3).
intersection([H|T1], S2, S3) :- intersection(T1, S2, S3).

union([], S, S).                                                                 %sjednocení dvou množin
union([H|T], S2, S3) :- union(T, S2, S4), add(H, S4, S3).

difference([], _, []).                                                           %rozdíl dvou množin
difference([H|T], S2, S3) :- member(H, S2), difference(T, S2, S3).
difference([H|T1], S, [H|T3]) :- not(member(H, S)), difference(T1, S, T3).

subset([], _).                                                                   %testuje, zda první množina je podmnožinou druhé
subset([H|T], S) :- member(H, S), subset(T, S).

equal(S1, S2) :- subset(S1, S2), subset(S2, S3).                                 %testuje rovnost množin
</code>

===== Lisp =====
==== Zásobník ====
<code lisp>
(defun push (E L) (cons E L))                                         ;vložení prvku

(defun pop (L)                                                        ;výběr prvku
       (cond ((null L) (cond ((print "error – stack is empty!") L)))
             ((print (car L)) (cdr L))))
</code>

==== Fronta ====
<code lisp>
(defun enqueue (E L) (append L (cons E nil)))                         ;vložení prvku

(defun dequeue (L)
       (cond ((null L) (cond ((print "error – queue is empty!") L)))  ;výběr prvku
             ((print (car L)) (cdr L))))
</code>

==== Fronta s prioritou ====
<code lisp>
(defun insert (E L)                                                   ;vložení prvku
       (cond ((null L) (cons E L))
             ((precedes E (car L)) (cons E L))
             (T (cons (car L) (insert E (cdr L))))))

(defun precedes (A B) (< A B))                                        ;platí pouze pro čísla!

(defun dequeue (L)
       (cond ((null L) (cond ((print "error – queue is empty!") L)))  ;výběr prvku
             ((print (car L)) (cdr L))))
</code>

==== Množina ====
<code lisp>
(defun add (E L)                                                   ;vložení prvku
       (cond ((member E L) L)
             (T (cons E L))))

(defun delete (E L)                                                ;výběr prvku
       (cond ((null L) L)
             ((equal E (car L)) (cdr L))
             (T (cons (car L) (delete E (cdr L))))))

(defun intersection (L1 L2)                                        ;průnik dvou množin
       (cond ((null L1) nil)
             ((member (car L1) L2)
                      (cons (car L1) (intersection (cdr L1) L2)))
             (T (intersection (cdr L1) L2))))

(defun union (L1 L2)                                               ;sjednocení dvou množin
       (cond ((null L1) L2)
             ((member (car L1) L2) (union (cdr L1) L2))
             (T (cons (car L1) (union (cdr L1) L2)))))

(defun difference (L1 L2)                                          ;rozdíl dvou množin
       (cond ((null L1) nil)
             ((member (car L1) L2) (difference (cdr L1) L2))
             (T (cons (car L1) (difference (cdr L1) L2)))))

(defun subset (L1 L2)                                              ;testuje, zda první množina je podmnožinou druhé
       (cond ((null L1) T)
             ((member (car L1) L2) (subset (cdr L1) L2))
             (T nil)))

(defun equal_set (L1 L2)                                           ;testuje rovnost množin
       (and (subset L1 L2) (subset L2 L1)))
</code>