zbychup
Dołączył: 17 Paź 2010
Posty: 130
Przeczytał: 0 tematów
Pomógł: 1 raz
Ostrzeżeń: 0/5
|
 Wysłany: Śro 23:38, 09 Lut 2011 Temat postu: Od kumpa z dziennych - nie ma jak judo ;) |
|
|
Podobno losujesz zestaw 5 pytań (na kazdy z 5 możliwych zestawów składa się 5 pytań w kolejnosaci co 5 z podanych zagadnień np zestaw nr1 to pytania 1,5,10,15,20,25).By zdać wystarczy odpowiedzieć na 3 z 5 pytań zestawu. Czyli żeby zdac wystarczy nauczyć się pierwszych 15 zadadnień... albo... jak kto woli ściagnąc (podobno wiekszośc z dziennych wybrała rozwiazanie nr 2  )
Opracowany material:
1. Definicje tautologii KRZ i tautologii (prawa) KRP. Podać przykłady.
Tautologią KRZ nazywamy formułę KRZ, która przyjmuje wartość logiczną
i dla każdego wartościowania zmiennych występujących w tej formule.
„jeżeli Poznań leży nad Wartą, to Poznań leży nad wartą” p → p
Mówimy, że formuła A jest prawem/tautologią KRP, jeżeli M |= A dla
każdej interpretacji M danego języka. Piszemy |=KRP A, |=KRP A
∀MM |= A
Prawa DeMorgana: ¬∀xΦ(x) ∃x¬Φ(x), ¬∃xΦ(x) ∀x¬Φ(x)
2. Stosunek wynikania logicznego w KRZ i KRP.
Mówimy, że formuła A logicznie wynika ze zbioru formuł S w KRZ jeżeli
każde wartościowanie spełniające zbiór S spełnia formułę A.
Mówimy, że formuła A logicznie wynika ze zbioru formuł S w KRP jeżeli
formuła A jest prawdziwa we wszystkich modelach zbioru S. Piszemy:
S |=KRP A. S |=KRP A ∀M(M |= S → M |= A)
3. Spełnialne zbiory formuł w KRZ i KRP; związki z wynikaniem logicznym.
Zbiór formuł S nazywamy spełnianym w KRZ, jeżeli istnieje wartościowanie,
które spełnia wszystkie formuły z tego zbioru. Formuła A logicznie
wynika ze zbioru formuł S wgdy zbiór S ∨ {¬A} nie jest spełnialny.
Zbiór formuł S nazywamy spełnianym w KRP, jeżeli istnieje model zbioru
S. Niech A będzie zdaniem. S |=KRP A wgdy zbiór S ∨ {¬A} nie jest
spełnialny.
1
4. Koniunkcyjna i alternatywna postać normalna, metody sprowadzania, kryteria
tautologiczności i spełnialności.
Formuła w koniunkcyjnej postaci normalnej (KPN) jest to koniunkcja
skończenie wielu klauzul (alternatyw elementarnych) np. (p ∨ ¬q ∨ r) ∧
(¬p ∨ ¬r).
Formuła w alternatywnej postaci normalnej (APN) jest to alternatywa
skończenie wielu koniunkcji elementarnych np. (p ∧ ¬q ∧ r) ∨ (¬pland¬r).
Sprowadzenie do APN i KPN metodą przekształceń równoważnościowych:
Podformuły danej formuły zastępujemy równoważnymi formułami, stosując
następujące prawa (zastępujemy lewą stronę prawą stroną)
¬¬A A
(A B) (A → B) ∧ (B → A)
(A → B) ¬A ∨ B
¬(A ∨ B) ¬A ∧ ¬B
¬(A ∧ B) ¬A ∨ ¬B
A ∧ (B ∨ C) (A ∧ B) ∨ (A ∧ C)
(B ∨ C) ∧ A (B ∧ A) ∨ (C ∧ A)
A ∨ (B ∧ C) (A ∨ B) ∧ (A ∨ C) ∨ A (B ∨ A) ∧ (C ∨ A)
Formuła w KPN taut. KRZ wgdy w każdej składowej klauzuli występuje
para przeciwnych literałów.
Formuła w APN jest spełnialna wtw, gdy w każdej składowej koniunkcji
elementarnej występuje para przeciwnych literałów.
5. Reguła rezolucji zdaniowej i twierdzenie o pełności rezolucji zdaniowej
(dowód).
Reguła rezolucji w rachunku zdań to reguła, na mocy której z dwóch
klauzul (alternatyw skończenie wielu literałów) A, B wynika klauzula C,
jeżeli w A występuje literał p, w B literał ¬p, a C składa się ze wszystkich
pozostałych literałów występujących w A lub B.
Twierdzenie o pełności rezolucji zdaniowej:
Zbiór klauzul S jest niespełnialny wtedy i tylko wtedy gdy, gdy S ⊢ RZ.
2
6. Sprowadzanie formuł KRP do preneksowej postaci normalnej i skolemizacja.
Forma preneksowa to taka postać formuły logicznej, w której wszystkie
kwantyfikatory przesunięte są na początek formuły. Inna jej nazwa to
przedrostkowa postać normalna.
Najpierw należy zmienić nazwy wszystkim zmiennym, które kolidują, na
przykład: (∀x.R(x)) → (∃x.R(x)) na (∀x.R(x)) → (∃y.R(y)) co w żaden
sposób nie zmienia znaczenia formuły. Następnie należy przenosić kwantyfikatory
coraz wyżej, zmieniając je na przeciwny za każdym razem, gdy
napotkają negację:
(∀x.R(x)) → (∃y.R(y))
(¬∀x.R(x)) ∨ (∃y.R(y))
∃x.(¬R(x) ∨ (∃y.R(y))
∃x.∃y.(¬R(x) ∨ R(y))
7. Procedura automatycznego dowodzenia twierdzeń metoda rezolucji.
Niech S będzie zbiorem klauzul, przyjmijmy, że S0 = S. Załóżmy, że utworzyliśmy
zbiór Si. Wybierz parę klauzul kolidujących C1,C2 ∈ Si, które
jeszcze nie były wybrane. Niech C będzie rezolwentą C1 i C2 zgodnie z
definicją reguły rezolucji. Niech Si+1 = Si ∪C. Jeśli C = , to zakończ algorytm
stwierdzając, ze S jest niespełnialny. Jesli Si+1 = Si dla wszystkich
możliwych wyborów klauzul kolidujących, to zakończ algorytm stwierdzając,
że S jest spełnialny.
8. Klauzule Horna i programy Horna.
Klauzula Horna jest to klauzula zawierająca dokładnie jeden literał pozytywny:
¬A1 ∨ . . . ∨ ¬An ∨ B albo ¬A1 ∨ . . . ∨ ¬An → B
Klauzule Horna dzielą się na:
fakty: B,→ B,B
reguły: A1 ∨ . . . ∨ An → B albo B A1 ∨ . . . ∨ An
Programem Horna nazywamy skończony zbiór klauzul Horna.
9. Najmniejszy model Herbranda programu Horna (definicja, lemat).
Niech P będzie programem Horna. Określamy interpretację Herbranda
MP = {A ∈ BP : P| =KRP A}.
Lemat:
MP jest najmniejszym modelem Herbranda programu P. MP |= P.
3
10. Algorytm unifkacji i twierdzenie o unifkacji.
Algorytm unifikacji:
Wejście: S = {E1, ...,En}, n 1, Ei – wyrażenia proste
(0) Przyjmij σ0 = ϵ. Dla k = 0, 1, 2 . . . wykonuj:
(1) Wyznacz zbiór Sσk . Jeżeli |Sσk
| = 1, to STOP; Wyjście σk.
Jeżeli |Sσk
| > 1, to wyznacz DSσk
i idz (2).
(2) Jeżeli nie istnieją x, t ∈ DSσk
takie, że x /∈
V (t), to STOP;
Wyjście NIE.
W przeciwnym razie wybierz taką parę x, t i przyjmij
σk+1 = σk[x/t]; wróć do (1) przy k:=k+1.
Tw. o unifikacji Dla dowolnego niepustego, skończonego zbioru S algorytm
unifikacji kończy pracę w skończonej liczbie kroków. Jeżeli zbiór S jest
unifikowalny, to algorytm zwraca najogólniejszy unifikator zbioru S. Jeżeli
zbiór S nie jest unifikowalny, to algoryt odp. NIE.
11. Reguła rezolucji liniowej, wyprowadzenie liniowe, refutacja liniowa.
Reguła rezolucji linowej ma postać :
A1, . . . ,Am, . . . ,An - cel G
B B1 , . . . ,Bk – wariant klauzuli C programu P
———————————————————————
(A1, . . . ,Am−1,B1, . . . ,Bk,Am+1, . . . ,An)σ – nowy cel
gdzie σ jest MUG/MGU zbioru {Am,B} tzn. Amσ = Bσ.
Wniosek reguły rezolucji liniowej nazywamy resolwentą liniową przesłanek.
Refutacja liniowa:
Liniową refutacją dla P ∪ G nazywamy skończone wyprowadzenie liniowe
(G0C1G1 . . .CnGn) takie, że Gn = 0.
12. Odpowiedź poprawna i odpowiedź obliczona.
Niech P będzie programem Horna, a G zadaniem. Odpowiedzią poprawną
dla P ∨{G} nazywamy podstawienie θ, ograniczone do zmiennych w V(G)
i takie P |=KRP (A1 ∨ . . . ∨ An)θ.
Niech P będzie programem Horna, a A atomem (niekoniecznie ustalonym).
Jeśli P |=KRP A, to ϵ jest odpowiedzią obliczoną dla P ∨ { A}.
13. Twierdzenie o poprawnosci rezolucji liniowej (dowód).
Każdą odpowiedz obliczona dla P ∪ {G} jest odpowiedzią poprawna dla
P ∪ {G}.
Dowód: Wykład 8.
4
14. Atomy sukcesu programu P; lemat.
Atom A ∈ Bp taki, że istnieje refutacja linowa dla P ∨ { A} nazywamy
atomem sukcesu programu P. Zbiór wszystkich atomów sukcesu p
oznaczamy Sp.
Lemat 3. Sp = Mp dla dowolnego programu Horna P.
(Objaśnienie i hooy)
Mp = Suma od i=0 do nieskonczoności Mpi (a to kurestwo: Mpi , to zbiór
wszystkich instancji faktów z P).
15. Twierdzenie o pełnosci rezolucji liniowej (dowód).
Dla każdej odpowiedzi poprawnej Θ dla P ∪ {G} istnieje odpowiedz obliczona
σdla P ∪{G} oraz podstawienie γ takie, że Θ = (σ, γ)V (G). Inaczej
odpowiedzi poprawne pokrywają się ze wszystkimi możliwymi konkretyzacjami
odpowiedzi obliczonych.
16. Reguły obliczeniowe i SLD-drzewo. Regułą obliczeniową nazywamy funcję
R, która każdemu zdaniu A1...Ak (w danym języku. Tak, to tak pojebanie
wszystko brzmi) przyporządkowuje linię R( A1 . . .Ak) ∈ {1 . . . k}.
Refutację liniową (G0,C1,G1, ...,Cn,Gn) nazywamy zgodną z regułą obliczeniową
R jeśli dla każdego j = 1...n. Gj powstaje z CjGj−1 na mocy
(R-RL) z wybranym atomem AR (GjC1) (Gj−1 = A1...Al)
Standardowe reguły obliczeniowe:
LEFT R(G) = 1
RIGHT R( A1 . . .Ak) = k
SLD-drzewo – drzewo wszystkich wyprowadzeń dla P ∨ {G} ustalonej
regule obliczeniowej R.
17. Definicje rodziny funkcji czesciowo rekurencyjnych i relacji rekurencyjnej.
Rodzine REK okreslamy jako najmniejsza rodzine funkcji czesciowych
(f(N0)n → N0) do której nalezą wszystkie funkcje podstawowe i ktora
jest zamknieta ze wzgledu na podstawianie rekursją prostą i operator
minimum. Elementy rodziny REK nazywamy funkcjami częściowo rekurencyjnymi.
R ⊂ (N0)n – n-arguemtnowa relacja na N0.
CR(X) = 1 jezeli R(X), 0 jezeli ¬R(X)
CR to funkcja charakterystyczna relacji R (całkowita, określona) Relację
tą nazywamy rekurencyjną jezeli CR ∈ REK.
5
18. Twierdzenie o obliczeniowej zupełności programów Horna (szkic dowodu).
Dla każdej częściowo rekurencyjnej funkcji f istnieje program Horna Pf ,
który oblicza funcję f.
Dowód(szkic)
1. Funkcje podstawowe są obliczalne przez programy Horna. zero(x) = 0
Pzero Pzero(x, 0)
zadanie : Pzero(Sk(0), y) – strzałka jest tylko w jedną strone i ni chuja
przed tym
odpowiedz obliczona [y/0]
19. λ-termy, aksjomaty i reguły dowodzenia rachunku lambda.
Aksjomaty:
α) M=N jeśli M ≡ αN (α – konwersja)
β) (λx ·M)N = M[x/N] (β – konwersja)
γ) λx ·Mx = M jeśli x ̸∈ V (M) (λ).
Termy:
Jeżeli x ∈ X to x jest lambda-wyrażeniem,
Jeżeli M jest lambda wyrażeniem i , to napis λx.M jest lambdawyrażeniem,
Jeżeli M oraz N są lambda wyrażeniami, to napis (NM) jest lambdawyrażeniem,
Wszystkie lambda-wyrażenia można utworzyć korzystając z powyższych
reguł.
Reguły dowodzenia Lambda:
M = M
M=N
N=M
{M=N N=P}
M=P
M=N
MP=NP
M=N
NP=MP
M=N
λxM=λxN
20. Twierdzenie o punkcie stałym i twierdzenie o de?nicjach rekurencyjnych.
Tw. o p. Stałym.
Dla dowolnego termu F istnieje term X taki, że λ ⊢ FX = X.
Tw. o def. Rekurencyjnych
Dla dowolnego termu M[f,
−→x ] istnieje kombinator F taki, że w rachunku
lambda F
−→X= M[F,
−→x ].
6
21. Logika kombinatorowa i definicja lambda abstrakcji.
Logika kominatorowa:
Symbole:
zmienne X,Y,Z
stałe: S, K
Termy:
zmienne
stałe
aplikacja
Aksjomaty:
(S) SXYZ = XZ(YZ)
(K) KXY = X
22. Twierdzenie o λ defniowalności funkcji rekurencyjnych (szkic dowodu).
Wszystkie całkowite funkcje rekurencyjne są λ – definiowalne.
Dowód:
Funkcje podstwowe są λ – definiowalne.
zero(n) =0.
Z ≡ λx · O λ ⊢ Zn = 0.
suc(n) = n + 1
S+ ≡ λX0 [false, x]
λ + S+n = [false, n] ≡ (n + 1)
πin(k1, . . . , kn) = ki
prin ≡ λX1, . . . ,Xn · X
λ ⊢ prink1, ..., kn = k1
23. Termy normalne, termy normalizowalne, redukcja, twierdzenie Churcha-
Rossera.
Term normalny
Term nazywamy normalnym jeżeli nie zawiera redeksów. Normalny = w
postaci normalnej.
Term normalizowany
Term nazywamy normalizowanym jeżeli istnieje term normalny taki, ze
λ ⊢ M = N. Wtedy N nazywamy postacia normlaną termu M.
Twierdzenie Churcha-Rossera
jeżeli M →∗
B N (jest redukowalna). M1 i M →∗
B M2 to istnieje term N,
że M1 →∗
B N i M2 →∗
B N.
24. Twierdzenie o nierozstrzygalności rachunku lambda (dowód).
Brak danych.
7
25. Maszyna RAM, programy, numery programów, wzór Kleene’ego.
Maszyna RAM jest modelem obliczeń. Składa się ona z programu - skończonego
ciągu rozkazów definiujących jej działanie - oraz nieograniczonego
zbioru rejestrów, z których każdy może przechowywać dowolną liczbę naturalną.
Rejestry indeksujemy liczbami naturalnymi. Rejestr o indeksie 0
zwyczajowo nazywany jest akumulatorem. Zbiór rejestrów nazywamy pamięcią
operacyjną. maszyna RAM posiada również dwie taśmy: wejściową
i wyjściową zawierające symbole skończonego alfabetu.
pamięć, złożoną z ponumerowanych kolejno komórek,
taśmę wejściową, z której maszyna odczytuje dane,
taśmę wyjściową, na którą maszyna zapisuje wyniki,
program, czyli skończony ciąg rozkazów, do wykonania.
Program składa się ze skończonego ciągu rozkazów, podobnych do języka
asemblera dzisiejszych procesorów - instrukcje te przechowywane są poza
pamięcią maszyny RAM.
WZÓR KLEENEGO, NUMERY?
8
Enjoy!!!!
Post został pochwalony 0 razy
|
|
a dałbyś radę wstawić gdzieś jakąś wersję w *.doc