M ETODY D OWODZENIA T WIERDZE ´ N I A UTOMATYZACJA R OZUMOWA ´ N
K
ONWERSATORIUM7:
P
OWTÓRKAV rok kognitywistyki UAM
Zada´n podobnych do ni˙zej podanych mo˙zna spodziewa´c si˛e na kolokwium, które przeprowadzimy 1 grudnia 2015.
1 Notacje
1. Przekształ´c formuł˛e w notacji infiksowej na odpowiadaj ˛ac ˛a jej formuł˛e w notacji prefiksowej (polskiej):
1. (p ∨ ¬r) → (q → (r → (s → (t ∧ ¬p))) 2. (((p → (q ∧ r)) → ¬r) → (s ∨ ¬p)) → t
Narysuj drzewo wszystkich podformuł dla podanych wy˙zej formuł.
2. Przekształ´c formuł˛e w notacji prefiksowej (polskiej) na odpowiadaj ˛ac ˛a jej for- muł˛e w notacji infiksowej:
1. EApqAKpqAKpN qKN pq
2. CCCpqCCCN rN strCuCCrpCsp
Narysuj drzewo wszystkich podformuł dla podanych wy˙zej formuł.
2 Postacie normalne
3. Podaj koniunkcyjn ˛a posta´c normaln ˛a formuł:
1. (q → r) → ((p → q) → (p → r)) 2. (p ↓ q) ↑ ¬(p ↓ q)
1
3 Tablice analityczne
4. Tablice analityczne dla logiki pierwszego rz˛edu:
1. Ustal, czy wniosek
∃x∀y (P (x, y) → P (y, x)) wynika tablicowo z przesłanki:
∀x∀y (P (x, y) → P (y, x)) ∧ ∃x∀y P (x, y).
2. Ustal, czy wniosek
∃x (P (x) ∧ Q(x, x)) wynika tablicowo z przesłanki:
∃x (P (x) ∧ ∀y (P (y) → Q(y, x))).
5. Tablice analityczne dla KRZ. Ustal czy zbiór formuł jest tablicowo niesprzeczny:
1. {p → ¬q, q → ¬r, s → q, p ∨ r, s}
2. {p → q, r → s, ¬p ∨ r, p ∧ ¬s}
4 Rezolucja
6. Ustal czy nast˛epuj ˛ace formuły posiadaj ˛a dowód rezolucyjny:
1. ((p → q) → (p → r)) → (p → (q → r)) 2. (p → q) → ((r → s) → ((p ∧ r) → (q ∧ s)))
7. Ustal czy z nast˛epuj ˛acych zbiorów formuł mo˙zna wyprowadzi´c rezolucyjnie klauzul˛e pust ˛a:
1. { p ∨ ¬q, r → q, ¬(s ∧ ¬r), s ∧ ¬p } 2. { p ∨ (r ∧ ¬q), q ∨ ¬r, ¬p }
2
5 Wa˙zne poj˛ecia i fakty
8. Podaj definicje nast˛epuj ˛acych poj˛e´c:
1. Zdaniowa własno´s´c niesprzeczno´sci.
2. Zdaniowy zbiór Hintikki.
3. Własno´s´c niesprzeczno´sci pierwszego rz˛edu.
4. Zbiór Hintikki pierwszego rz˛edu.
9. Sformułuj twierdzenia:
1. Lemat Königa.
2. Twierdzenie o Istnieniu Modelu w KRZ.
3. Twierdzenie o Dedukcji (wprost, w KRZ).
4. Twierdzenie o Zwarto´sci (w KRZ).
Ka˙zde zadanie powinno ko´nczy´c si˛e wyra´znie sformułowan ˛a odpowiedzi ˛a. Pro- sz˛e pisa´c wyra´znie. Dowody powinny zawiera´c informacj˛e dowodow ˛a (które kroki otrzymywane s ˛a z których).
Jerzy Pogonowski Zakład Logiki i Kognitywistyki UAM www.kognitywistyka.amu.edu.pl http://logic.amu.edu.pl/index.php/Dydaktyka pogon@amu.edu.pl
3
