Abychy mohl rezolvovat, musím:

1. Disjunktivní normální forma (a ∨ b ∨ c ∨ d)
2. 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)))
3. 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)))

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

1. {učil(x), ¬umí(x)}
2. {¬umí(x), body(x)}
3. {¬body(x), zkouška(x)}
4. {zkouška(a)}
5. {¬učil(a)}
6. {¬zkouška(x), umí(x)}

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

push(E, T, [E|T]).  %vložení prvku
 
pop(E, [E|T], T).   %výběr prvku

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

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

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

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

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

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

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