Kalábovi

Kalábovic wikina

Uživatelské nástroje

Nástroje pro tento web


pitel:izu:isz

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 A1 ∧ A2 ∧ … ∧ An ⇒ Ai; i ∈ <1, n>
14 Zavedení OR Ai ⇒ A1 ∨ A2 ∨ … ∨ An; 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:

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

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

  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]
  • {}

Prolog

Zásobník

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

Fronta

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

Fronta s prioritou

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

Množina

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

Lisp

Zásobník

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

Fronta

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

Fronta s prioritou

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

Množina

(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)))
/var/www/wiki/data/pages/pitel/izu/isz.txt · Poslední úprava: 03. 07. 2012, 13.53:43 (upraveno mimo DokuWiki)