Microsoft Word - programowanie_deklaratywne

1. Podaj określenie wartościowania w KRZ i jego rozszerzenia na dowolne formuły. Podaj przykład wartościowania formuły w KRZ.

Def. Wartościowanie.
1. Wartości logiczne : 1 (prawda), 0 (fałsz)
2. Wartościowaniem nazywamy funkcję w: V{0, 1};
gdzie

V = {p, q, r,...,p

,...,p’,...} - nieskończony, ale przeliczalny zbiór zmiennych zdaniowych

3. Funkcją logiczną nazywamy funkcję f: {0, 1}

 {0, 1}.

Określamy funkcje: f



:{0,1}{0,1} i f



, f



, f



, f



:{0,1}

{0,1} następująco:

x y f



(x)



(x, y)



(x, y)



(x, y)



(x, y)

1
1
0
0

1
0
1
0

0
0
1
1

1
0
0
0

1
1
1
0

1
0
1
1

1
0
0
1

4. Każde wartościowanie w: V  {0,1} rozszerzamy do funkcji ŵ FOR  {0,1}, (ŵ(A) – wartość logiczna formuły A przy
wartościowaniu w) następująco:

ŵ(p) = w(p) dla p

V

ŵ (

A) = f

(ŵ(A))

ŵ(A

B) = f



(ŵ(A), ŵ(B))

ŵ(A

B) = f



(ŵ(A),ŵ(B))

ŵ(AB) = f



(ŵ(A),ŵ(B))

ŵ(A

B) = f



(ŵ(A),ŵ(B))

Przykład 1.2. Wartościowanie formuł.
Formuła A: p  q

 r. Wartościowanie: w(p)=1, w(q)=0, w(r)=1.

ŵ(A) = ŵ(p q

 r ) = f



(ŵ(p), ŵ(q

 r )) = f



(ŵ(p), f



(ŵ (q), ŵ (r))) = f



(w(p),f



(w(q), w(r))) = f



(1, f



(0,1)) = f



(1,1) = 1

2. Podaj określenia następujących pojęć w KRZ: spełnialność formuły i zbioru formuł przez wartościowanie, formuła spełnialna,
zbiór spełnialny. Wykaż, że następujące warunki są równoważne: a) formuła A jest tautologią KRZ b) formuła (

A) nie jest

spełnialna.

Def. Spełnianie formuły i zbioru formuł przez wartościowanie.
1. Wartościowanie w spełnia formułę A (oznaczenie: w |= A), jeżeli ŵ (A) = 1.
2. Wartościowanie w spełnia zbiór formuł

  FOR (ozn. w |=  ), jeżeli ŵ (A) = 1 dla każdej formuły A  .

Def. Spełnialność formuły i zbioru formuł.
1. Formułę A nazywamy spełnialną, jeżeli istnieje wartościowanie w takie, że w |= A.
2. Zbiór formuł

  FOR nazywamy spełnialnym, jeżeli istnieje wartościowanie w takie, że w |= .

Def. Tautologia KRZ
Tautologią rachunku zdań nazywamy formułę A taką, że ŵ (A) = 1 dla każdego wartościowania w.
Fakt 1.1
Następujące warunki są równoważne:

a) formuła A jest tautologią KRZ
b) formuła (

A) nie jest spełnialna

Dowód faktu 1.1

a) należy udowodnić za pomocą tabeli wartościowania, że kadże wartościowanie daje prawdę
b) należy wskazać, że żadne wartościowanie nie spełnia

A, zatem A nie jest spełnialna czyli A jest tautologią KRZ

3. Omów wynikanie logiczne w KRZ. Podaj określenie logicznej reguły wnioskowania w KRZ i reguły rezolucji zdaniowej. Wykaż,
że reguła rezolucji zdaniowej jest logiczną regułą wnioskowania.

Def. Wynikanie logiczne.
Formuła A wynika ze zbioru formuł

 w KRZ, jeżeli dla każdego wartościowania w zachodzi warunek: jeżeli w |= , to w |= A.

Fakt 1.2.
Następujące warunki są równoważne:
a)

formuła A wynika ze zbioru formuł

 w KRZ

zbiór

  (A ) nie jest spełnialny.

Fakt 1.3.
Następujące warunki są równoważne:
a)

formuła A wynika ze zbioru formuł {A

, ..., A

}

formuła A

 ...  A

 A jest tautologią KRZ

Def. Logiczna reguła wnioskowania.
Jeżeli ze zbioru formuł {A

, ..., A

}, które będziemy nazywać przesłankami wynika formuła A, którą będziemy nazywać wnioskiem,

to schemat

nazywamy logiczną regułą wnioskowania.
Def. Literały.
Literałem pozytywnym nazywamy dowolną zmienną zdaniową p

 V , a literałem negatywnym negację zmiennej zdaniowej p, p

 V.
Literały oznaczamy: L

, L

, ....

Reguła rezolucji zdaniowej

, L

, ..., L

, p}

’

, L

’

, ..., L

’

 p}

__________________

, L

, ..., L

’

, L

’

, ..., L

’

} n,m

 0

Fakt 1.6.
Reguła rezolucji zdaniowej jest logiczną regułą wnioskowania, tzn. wniosek reguły rezolucji zdaniowej wynika ze zbioru przesłanek
tej reguły.
Dowód
Zał., że istnieje wartościowanie w spełniające obie przesłanki: w |= {L

, L

,..., L

, p} w |= {L

’, L

’,..., L

’,

p}

Rozważmy dwa przypadki:
1. w(p)=1, wtedy w(

p)=0, tzn w|(p), stąd w(L’

)=1 dla pewnego 1

 i n. Zatem w spełnia wniosek w |= {L

’, L

’,..., L

’ }

2. w(p)=0, wtedy istnieje 1

 j m takie, że w(L

)=1. Zatem w spełnia wniosek w |= {L

, L

,..., L

}

4. Podaj określenie derywacji klauzuli ze zbioru klauzul oraz refutacji zbioru klauzul w KRZ. Podaj przykład derywacji i refutacji.

Def. Klauzule.
Klauzulami nazywamy skończone zbiory literałów.
Klauzulę {L

, L

,..., L

} interpretujemy jako alternatywę L

 L

... L

Klauzule oznaczamy: A, B, C, ...; klauzula pusta: ;

- zbiór klauzul

Def. Drzewo binarne.
Drzewem binarnym nazywamy skończony i niepusty zbiór X

 {0,1}

spełniający warunki:

a) jeżeli xy

 X, to x  X,

b) jeżeli x

 X, to (x0  X  x1  X ); warunek ten mówi, że istnieją dwa lub zero potomków (następników).

Elementy zbioru X nazywamy wierzchołkami drzewa. W szczególności:

 nazywamy korzeniem drzewa X;

elementy

 X, takie że x0  X i x1  X , to liście drzewa;

wierzchołki x0, x1

 X nazywamy bezpośrednimi potomkami wierzchołka x  X.

Def. Drzewo etykietowane.
Etykietowanym drzewem binarnym nazywamy trójkę (X, E, f ) taką, że X jest drzewem binarnym, E jest niepustym zbiorem, a f –
funkcją , f: X

 E. Elementy zbioru E nazywamy etykietami, f (x) jest etykietą wierzchołka x.

Def. Derywacja klauzuli ze zbioru klauzul.
Derywacją klauzuli A ze zbioru klauzul

 nazywamy drzewo etykietowane (X, E, f) takie, że:

E jest zbiorem klauzul

;

dla

każdego liścia x drzewa X, f (x)

;

f (

)= A ;

dla

każdego wierzchołka x drzewa X nie będącego liściem f (x) jest rezolwentą etykiet bezpośrednich potomków

wierzchołka x.
Przykład
1)

={{p, q},{p, q}}

 |–

{q}:

// derywacja {q} z

; poniżej mamy drzewo etykietowane, gdzie korzeń drzewa to {q};

Przykład
Niech

 = { {p, q, r}, {p, q, r }, {q, r}, {q, r} }. Przykład derywacji (wyprowadzania)  |–

(p, r):

Def. Refutacja zbioru klauzul.
Derywację klauzuli pustej ze zbioru klauzul

 nazywamy refutacją zbioru .

Przykład

={{p, q},{p, q},{p, q},{p, q}}

{p, q} {

p, q}

\ /

{q}

f(0,0)={p, q, r} {p, q,

r}=f(0,1)

f(0)={p, q} {

q, r}=f(1)



{p, r}=f(

)

|–

5. Uzasadnij algorytm sprawdzania tautologiczności formuł KRZ za pomocą rezolucji zdaniowej.

Algorytm 1.2. Sprawdzanie tautologiczności formuł KRZ za pomocą rezolucji zdaniowej.
Dane : formuła A
Wynik : odpowiedź tak, jeżeli formuła A jest tautologia KRZ, odpowiedź nie w przeciwnym przypadku
(1) bierzemy formułę B identyczną z formułą (

A).

(2) sprowadzamy formułę B do koniunkcyjnej postaci normalnej KPN(B)
(3) formułę KPN(B) przedstawiamy w postaci klauzulowej

(KPN(B))

(4) szukamy derywacji klauzuli pustej ze zbioru

(KPN(B))

(5) jeżeli klauzula pusta została otrzymana, odpowiedź tak
(6) jeżeli algorytm zatrzymał się ze względu na brak możliwości stosowania reguły rezolucji, odpowiedź nie.
Fakt 1.1 – patrzy odp. 2
Fakt 1.8
Następujące warunki są równoważne:

(i)

w |= A

(ii)

w |= KPN(A)

(iii)

w |=

(KPN(A))

Tw. 1.3 O zgodności i pełności rezolucji zdaniowej
Następujące warunki są równoważne:

1) zbiór

 nie jest spełnialny

 |-

Uzasadnienie
A

jest

tautologią KRZ



fakt 1.1

A jest nie spełnialna



fakt 1.8

KPN(

A) nie jest spełnialna



fakt 1.8

(KPN(A)) nie jest spełnialna



tw 1.3 o zgodności i pełności rezolucji zdaniowej

(KPN(A)) |–

Przykład
Czy formuła A: (pq)  (

q  p) jest tautologią KRZ ?

Stosujemy algorytm 1.2
1. Zamieniamy problem na zadanie równoważne:
Czy formuła:

A: [(pq)(q  p )] jest niespełnialna.

2. Formułę powyższą sprowadzamy do postaci KPN:
[(pq)  (q  p)]

[(p  q)  (q  p) ]
[ (p  q)  (q  p) ]

(p  q)  (q  p)
(

p  q)  (q  p)

KPN(

A) : (p  q)  q  p

3. KPN(

A) zapisujemy w postaci zbioru klauzul: ( KPN (A) ) = {{p, q}, { q}, {p} }.

4. Ze zbioru

( KPN (A) ) staramy się wyprowadzić klauzulę pustą:

Odp.

A nie jest spełnialna, zatem A jest tautologią (wszystkie wartości spełniają A).

Przykład
Czy formuła A: p

 q  p  q jest tautologią KRZ ?

A: ( p  q  p  q )

2. KPN (

A)::

[(p  q)  (p  q) ]

 q)  (p  q)

 q)  (p  q) = KPN (A)

{p, q} (

p, q} {p, q} {p, q}

\ / \ /

{q} {

q}

\ /

Uwaga: jedną klauzulę
stosujemy tylko raz

{

p, q} {q}

\ /
{

p} {p}

\ /

 (KPN (A) ) = {{p, q}, {p, q}}

4. {{p, q}, {

p, q}} |–

Odp. Nie można dalej stosować reguły rezolucji, tzn. nie istnieje refutacja zbioru

 (KPN (A) ), zatem A nie jest tautologią.

6. Podaj określenie języka pierwszego rzędu oraz termów, formuł atomowych, formuł, zdań, termu bazowego i atomu bazowego.

Def. Język pierwszego rzędu.
Symbole
a) logiczne

– zmienne przedmiotowe: x, y, z,..., x’,..., x

,...

VAR – zbiór wszystkich zmiennych przedmiotowych

–

stałe logiczne:

, , , , , , 

– symbole pomocnicze: ( , )

b) pozalogiczne

– symbole relacyjne (predykaty): P, Q, R, ...

– symbole funkcyjne: f, g, h, ...

–

stałe przedmiotowe: a, b, c, ...

Językiem pierwszego rzędu nazywamy układ L = ( R

, ..., R

; f

, ..., f

; a

, ..., a

;

)

gdzie: R – relacje, f – funkcje, a – stałe,

 jest funkcją , która dla każdego symbolu relacyjnego i funkcyjnego określa jego arność, tzn.

liczbę argumentów, przy czym

(R

)> 0, i=1,2,...,n oraz

(f

)> 0, i=1,2,...,m.

Def. Termy.
Termami języka L nazywamy wyrażenia określone przez następujące warunki:
–

każda zmienna i stała przedmiotowa jest termem,

–

jeżeli f jest symbolem funkcyjnym,

 (f) = n oraz t

,..., t

są termami, to f ( t

,..., t

) jest termem.

TER

– zbiór wszystkich termów języka L.

Def. Formuły atomowe.
Formułami atomowymi (atomami) języka L nazywamy wyrażenia postaci R ( t

,..., t

), gdzie R jest symbolem relacyjnym,

 (R) = n,

a t

,..., t

są termami.

Def. Formuły
Formułami języka L nazywamy wyrażenia określone przez następujące warunki:
–

każda formuła atomowa jest formułą,

– jeżeli A i B są formułami, to wyrażenia (

A), (A  B), (A  B), (A  B), (A  B) są formułami,

–

jeżeli A jest formułą i x jest zmienną przedmiotową, to wyrażenia (

x A), (x A) są formułami.

FOR

– zbiór wszystkich formuł języka L.

Def. Zdania.
Zdaniem (formułą domkniętą) nazywamy formułę bez zmiennych wolnych.
SEN

– zbiór wszystkich zdań języka L.

Niech

V(A)– zbiór wszystkich zmiennych wolnych w formule A.

V(t)– zbiór wszystkich zmiennych występujących w termie t.

Def. Termy bazowe.
Termem bazowym nazywamy term nie zawierający zmiennych.
TB

– zbiór wszystkich termów bazowych języka L.

Def. Atomy bazowe.
Atomem bazowym nazywamy formułę atomową nie zawierającą zmiennych.
AB

– zbiór wszystkich atomów bazowych języka L.

Przykład
Język: L = ( Q/1; P/2; R/2; f/2; g/1; a, b, c)
Termy: x, y, z, a, b, f(x, y), g(a), f(a, g(x)), ...
Formuły atomowe: Q(a), P(x, c), R(f(x, y), g(b)), ...
Formuły: Q(a)

 P(x, c); x P(x, c); x y [P(x, y)  Q(y)]; ...

Zdania: P(a, b)

 x Q(a); R(a, b)  Q(a); ...

Termy bazowe: a, b, c, f(a, b), ...
Atomy bazowe:Q(c), P(a, c), R(a, a), R(f(a, b), g(a)), ...

7. Podaj określenia następujących pojęć w LPR: zdanie, domknięcie formuły, prawdziwość formuły w interpretacji.

Def. Zdania.
Zdaniem (formułą domkniętą) nazywamy formułę bez zmiennych wolnych.
SEN

– zbiór wszystkich zdań języka L.

Def. Domknięcie formuły.
Niech A będzie formułą o zbiorze zmiennych wolnych V (A) = {x

,..., x

{p, q} {

p, q}

\ /
{q}

Domknięcie uniwersalne formuły A:

x

...

x

Domknięcie egzystencjalne formuły A:

x

...

x

Domknięcie uniwersalne i egzystencjalne formuły A jest zdaniem.
Def. M |= A. A – formuła.
Formuła A jest prawdziwa w interpretacji M lub inaczej: interpretacja M spełnia formułę A (M |= A), jeżeli jej domknięcie uniwersalne
jest prawdziwe w M.
Formuła A jest spełnialna jeżeli istnieje interpretacja, która ją spełnia..

8. Podaj definicję i własności podstawienia. Na czym polega złożenie podstawień? Podaj przykład.

Def. Podstawienie.
Podstawieniem nazywamy funkcję

: VAR  TER

. Stosujemy notację postfiksową: zamiast

 (x) piszemy x.

Dziedzina podstawienia: DOM (

) = {xVAR: x  x }.

 – podstawienie identycznościowe: x = x dla wszystkich xVAR, DOM() = .
Podstawienie naz. skończonym, jeśli jego dziedzina jest skończona, tzn. DOM (

) = {x

,..., x

}. Jeżeli dla tego podstawienia x

 = t

, i

= 1, 2,..., n , to podstawienie to przedstawiamy jako zbiór przypisań:

 = {x

,..., x

Podstawienie złożone:
Niech:

 = {y

,…, y

 = {x

,…, x

}. Podstawienie

 otrzymujemy ze zbioru {y



,…, y

 , x

,…, x

}

przez usunięcie:
- elementów y

/ s

 takich, że y

= s



- elementów x

/ t

takich, że x

 {y

,…, y

}

Własności podstawienia:

x (

) = (x)

() = ()

 =  = 

Przykład
a) Podstawianie:
A: P(x,y,f(a,y)),

 = { x/b, y/a }

 = P(x,y,f(a,y)) 

= P(x

, y, f(a,y)

) = P(x

, y, f(a

)) = P(b,a,f(a,b))

b) Składanie podstawień:
 = { x/f(y), y/z, u/g(u) },  = { x/a, y/b, z/y, u/c }

 = { x/f(y), y/z, u/g(u); x/a, y/b, z/y, u/c } = { x/f(b), y/y, u/g(c); x/a, y/b, z/y, u/c } = { x/f(b), u/g(c); y/b, z/y }
c)

  

 = { x/f(y), y/z }, = { x/a, z/b }

 = { x/f(y), y/b; x/a, z/b } = { x/f(y), y/b, z/b }

 = { x/a, z/b; x/f(y), y/z } = { x/a, z/b, y/z }

9. Podaj określenie interpretacji języka pierwszego rzędu.

Niech L = ( R

, ..., R

; f

, ..., f

; a

, ..., a

;

) będzie językiem pierwszego rzędu.

Def. Interpretacja języka.
Interpretacją języka L nazywamy układ

M = (|M|; R

, ..., R

; f

, ..., f

; a

, ..., a

) gdzie

|M| – niepusty zbiór zwany dziedziną lub uniwersum interpretacji,
R

– n-argumentowa relacja na zbiorze |M|, n =

(R

), tzn. R

 |M|

= { (u

, ..., u

) : u

, ..., u

 |M|},

– n-argumentowe działanie na zbiorze |M|, n =

(f

), tzn. f

: |M|

-> |M|,

- element zbioru |M|.

Dla każdego termu bazowego języka L, t

TB

, tzn. termu nie zawierającego zmiennych, określamy t

 |M| następująco:

jest dane przez interpretację M,

,...,t

))

= f

,...,t

Przykład
Język: L = (p/2, f/2, g/2; a,b);
Interpretacja: M

= (N; =

; +

;0,1). Uniwersum interpretacji: |M

| = N = {0,1,2,3,...}

(m,n) = m=n,

(m,n) = m+n,

(m,n) = m*n,

= 0, b

= 1.

Term: t = f(g(a,a),g(b,b))
t

= f

, a

), g

, b

)) =

, a

) + g

, b

) = 0 * 0 + 1 * 1

10. Wykaż, że następujące warunki są równoważne:

a) formuła A jest tautologią LPR,
b) formuła

A nie jest spełnialna.

…………

!!! nie było dowodzone na wykładzie (fakt 2.1) !!!

…………………

11. Wykaż, że następujące warunki są równoważne:

a) formuła A wynika logicznie ze zbioru formuł

 w LPR

b) zbiór

 (A) nie jest spełnialny.

…………

!!! nie było dowodzone na wykładzie (fakt 2.2) !!!

…………………

12. Podaj określenie wyrażenia prostego, przemianowania zmiennych, wariantów wyrażenia prostego. Każde pojęcie zilustruj
przykładem

Def. Wyrażenia proste
Wyrażeniem prostym nazywamy termy i atomy (formuły atomowe).
Wprowadzamy oznaczenia:

E – wyrażenie proste
V(E) – zbiór zmiennych występujących w E
σ|V(E) – ograniczenie podstawienia σ do zbioru V(E);
jest to podstawienie η takie, że
xη=xσ dla x

V(E)

xη=x dla x

V(E)

Def. Przemianowanie zmiennych
Przemianowaniem zmiennych nazywamy podstawienie σ takie, że
σ|V(E):V(E) →(1-1) VAR
xη=x dla x

V(E)

Przykład przemianowania
Wyrażenia:
E=P(f(x,y),g(z))
F=P(f(y,x),g(u))
są swoimi wariantami ponieważ
η={x/y,y/x,z/u}
η|V(E) jest 1-1 (różnowartościowe)
Eη=F
oraz dla
σ={y/x,x/y,u/z}
σ|V(E) jest 1-1 (różnowartościowe)
Fσ=E

Def. Wariant wyrażenia prostego
Jeżeli σ jest przemianowaniem zmiennych w wyrażeniu E, to wyrażenie Eσ nazywamy wariantem wyrażenia E.

Przykład stworzenia wariantu dla przemianowania
E=P(f(x),y,z)
V(E)={x,y,z}
Podstawienie σ={x/y,y/x} daje Eσ=P(f(y),x,z)

13. Podaj określenie wynikania logicznego w LPR i sformułuj warunki konsekwencji, jakie spełnia wynikanie logiczne.

Def. Model zbioru formuł.
Interpretację M nazywamy modelem dla zbioru formuł



, jeżeli wszystkie formuły ze zbioru



są prawdziwe w M, co oznaczamy

przez

M |

 

Def. Wynikanie logiczne.
Formuła A wynika logicznie ze zbioru formuł



, jeżeli formuła A jest prawdziwa we wszystkich modelach dla zbioru



Wprowadzamy oznaczenie Γ|=

LPR

A – formuła A wynika logicznie ze zbioru Γ na gruncie LPR.

Fakt
Wynikanie logiczne na gruncie LPR spełnia warunki konsekwencji tzn.:
(C1) jeżeli A

Γ, to Γ|=

LPR

(C2) jeżeli Γ

Δ oraz Γ|=

LPR

A to Δ |=

LPR

(C3) jeżeli Γ|=

LPR

Ai dla wszystkich 1<=i<=n oraz A1,…,An |=

LPR

A to Γ|=

LPR

14. Podaj określenie formuły w preneksowej postaci normalnej. Jaki jest związek między formułą A i PNF(A) ?

Def. Preneksowa postać normalna.
Formuła LPR znajduje się w preneksowej postaci normalnej (PNF), jeżeli jest postaci

...Q

// A – matryca Q… - prefix

gdzie Q

,...,Q

 {,}, zaś formuła A nie zawiera kwantyfikatorów.

Tw. 2.1.
Dla każdej formuły A istnieje formuła B w preneksowej postaci normalnej, która jest logicznie równoważna formule A, tzn. każda
interpretacja M spełnia formułę



15. Podaj określenie formuły w postaci Skolema. Jaki jest związek między formułą A i SKOL(A) ?

Def. Postać Skolema formuły LPR.
Formuła A jest w postaci Skolema (SKOL(A)), gdy jest w preneksowej postaci normalnej, a jej prefiks nie zawiera kwantyfikatorów
egzystencjalnych.
Tw. 2.2.
Formuła A jest słabo równoważna formule SKOL(A), tzn. formuła A jest spełnialna wtedy i tylko wtedy, gdy spełnialny jest jej
odpowiednik Skolema, SKOL(A).

16. Co rozumiemy przez konkretyzację formuły (klauzuli) w LPR? Czym jest gr(

) dla zbioru klauzul ? Podaj twierdzenie

dotyczące

 i gr().

Def. Konkretyzacja formuły.
Każde podstawienie formuły (klauzuli) nazywamy przykładem lub konkretyzacją tej formuły (klauzuli).
Jeżeli podstawienie to jest podstawieniem bazowym, to i konkretyzację nazywamy bazową lub ustaloną.

Niech

– zbiór klauzul

gr(

) – zbiór wszystkich ustalonych konkretyzacji klauzul ze zbioru



Tw. 2.3.
Dla każdego zbioru klauzul



następujące warunki są równoważne:

zbiór

 jest spełnialny,

zbiór

gr(

) jest spełnialny.

Dowód
(

 )

Załóżmy, że

 jest spełnialny, tzn. istnieje struktura M taka, że 



M |= A

Elementami zbioru gr(

) są klauzule postaci A[x

, ... , x

] dla A

.

Na podstawie prawa LPR

x A  A[x/t] mamy: x A  A[x

, ... , x

] jest tautologią LPR.

Zatem





M |= A[x

, ..., x

] czyli M |= gr(

) jest spełnialny.

P(x, y) : P(a, a), P(a, b), P(b, a), P(b,b) – wszystkie konkretyzacje języka

P(f(a), a), P(f(f(a)), a), ... – bardzo dużo konkretyzacji gdy w języku jest dostępny symbol funkcyjny.

(

 )

Zakładamy, że gr(

) jest spełnialny.

Istnieje struktura M taka, że M |= gr(

). Tworzymy strukturę N następująco:

za nośnik tej struktury przyjmujemy | N | - zbiór wszystkich ustalonych termów języka.
a

= a

, ..., t

) = f(t

, ..., t

)

, ..., t

) = P

, ..., t

)

Stąd dla każdego zdania ustalonego A mamy: M |= A

 N |= A , czyli N |= gr(). Zatem  jest spełnialny.

17. Uzasadnij algorytm dowodzenia praw w LPR za pomocą rezolucji zdaniowej.

Algorytm 2.3. Sprawdzanie tautologiczności formuł LPR z wykorzystaniem rezolucji zdaniowej
Dane: formuła A
Wynik: odpowiedź tak, jeżeli A jest tautologią oraz nie w przeciwnym przypadku
(1) niech B będzie formułą PNF(

A)

(2) znajdujemy formułę SKOL(B)
(3) w formule SKOL(B) opuszczamy kwantyfikatory i jeżeli nie jest w postaci KPN, to sprowadzamy ją do tej postaci otrzymując
formułę C.
(4) formułę C przedstawiamy w postaci klauzulowej

(C)

(5) szukamy derywacji klauzuli pustej ze zbioru gr(

(C))

(6) jeżeli klauzula pusta została otrzymana: odpowiedź tak
(7) jeżeli algorytm zatrzymał się ze względu na brak możliwości stosowania reguły rezolucji, odpowiedź nie.
Uwaga!! Algorytm 2.3

 daje odpowiedź tak wtedy i tylko wtedy, gdy formuła A jest tautologią LPR

 gdy formuła A nie jest tautologią LPR daje odpowiedź nie lub się zapętla.

Fakt 2.1 – patrz odp. 10
Tw. 2.1 – patrz odp. 14
Tw. 2.2 – patrz odp. 15
Def .Spełnialności – patrz odp. 2

Tw. 2.3 – patrz odp. 16
Tw. 2.4
Dla każdego zbioru zdań ustalonych

 następujące warunki są równoważne:

a) zbiór

 jest spełnialny w sensie (zakresie) LPR (tzn. przez interpretację)

b) zbiór

 jest spełnialny w sensie rachunku zdań (tzn. przez wartościowanie)

Uzasadnienie

Formuła A jest tautologią LPR



Fakt 2.1

A jest nie spełnialna



Tw. 2.1

PNF(

A) nie jest spełnialna



Tw. 2.2

SKOL(PNF(

A)) nie jest spełnialna // oznaczamy ją B



def. Spełnialności

C = matryca (B) nie jest spełnialna



Zbiór klauzul

(C ) nie jest spełnialny



Tw. 2.3

Zbiór klauzul gr(

(C )) nie jest spełnialny



Tw. 2.4

Istnieje refutacja zbioru gr(

(C )), tzn. istnieje wyprowadzenie klauzuli pustej ze zbioru gr((C )), za pomocą rezolucji

zdaniowej

18. Podaj określenie zbioru niezgodności dla zbioru wyrażeń prostych i zilustruj przykładem.

[ Dygresja: Wyrażeniami prostymi nazywamy termy i atomy (formy atomowe) ]

Zbiór niezgodności.
Niech S będzie skończonym zbiorem wyrażeń zawierających więcej niż jedno wyrażenie:
S = {E

... , E

}, n

 2

Zbiór niezgodności D dla zboru S wyznaczamy następująco . Znajdujemy pierwszą od lewej pozycję, na której przynajmniej 2
wyrażenia zbioru S mają różne symbole. Na tej pozycji znajduje się stała, zmienna, symbol funkcyjny lub symbol relacyjny. Z
każdego wyrażenia do zbioru D włączamy to podwyrażenie, które zaczyna się od znalezionej pozycji.

a) S = { P(x,f(y)), P(x,g(z)) }
D = { f(y), g(z) }

b) S = { P(f(x),h(y),e), P(f(x),z,e), P(f(x),h(y), b) }
D = { h(y), z }

[Jeżeli D, jest zbiorem niezgodności dla S, to jeżeli

 unifikuje zbiór S, to unifikuje D // brak pytań o unifikację – nie uczyć się]

19. Podaj algorytm wyznaczania najbardziej ogólnego unifikatora zbioru wyrażeń oraz twierdzenie o unifikacji.

[ Dygresja:
Def. Najogólniejszy unifikator zbioru wyrażeń MGU (most general unifier)
Podstawienie

 nazywamy najogólniejszym unifikatorem zbioru S, jeżeli spełnia warunki:

 jest unifikatorem zbioru S

b) dla każdego unifikatora

 zbioru S istnieje podstawienie  takie, że,  = 

]

Algorytm 3.1 Algorytm unifikacji – procedura poszukiwania MGU
Wejście: skończony zbiór wyrażeń prostych S
Wyjście: MGU dla S, jeśli S jest zunifikowany, NIE w przeciwnym wypadku.

1) k

= 0,





2) Wyznaczamy zbiór S



Jeżeli S



jest jednoelementowy, to STOP;

Wyjście:



. W przeciwnym wypadku wyznaczamy zbiór niezgodności D

dla S



3) Wybieramy w zbiorze D

parę x, t, taką, że x

 VAR, t  TER oraz x  V(t), przyjmijmy 

k+1



{x/t}, wracamy do punku

2. Algorytm przy k=k+1, Jeżeli nie ma takiej pary, to STOP, wyjście nie.

Twierdzenie 3.1 O Unifikacji.
Jeżeli zbiór S jest unifikowany, to algorytm kończy pracę z wyjściem będącym MGU zbioru S. Jeżeli S nie jest unifikowany, to
algorytm kończy pracę z wyjściem nie.

20. Podaj określenie klauzuli definitywnej, programu definitywnego, klauzuli celu, klauzuli Horna.

Klauzulą definitywną nazywamy klauzulę zawierającą dokładnie jeden pozytywny literał, co zapisujemy:
B

, ..., B

-> A, gdzie B

, ..., B

= B

 B

 ...  B

w szczególności:
n = 0 : -> A – klauzula jednostkowa – Fakt (1->A)
n > 0 : B

, ..., B

-> A – klauzula nie jednostkowa: REGUŁA, co zapisujemy jako:

A <- B

, ..., B

, gdzie A to głowa, B

, ..., B

, - body – ciało reguły

Programem definitywnym nazywamy dowolny skończony zbiór klauzul definitywnych, tzn. zbiór o postaci:

( B

, ..., B

-> A).

Klauzulą celu nazywamy klauzulę nie zawierającą literałów pozytywnych, co zapisujemy: <- B

, ..., B

, które jest równoważne

formule:

(( B

 ...  B

)), z KRZ (p -> 0) ->

p

Klauzula Horna to klauzula definitywna lub klauzula celu zawierająca co najwyżej jeden literał pozytywny.

21. Omów strategię Prologu.

Niech P będzie programem definitywnym, a G celem. Bierzemy pod uwagę zbiór P

 {G}. Jeżeli wykażemy, że zbiór P {G} nie

jest spełnialny, to na podstawie F.2.2 (patrz odp. 11) otrzymamy, że formuła

G wynika logicznie ze zbioru formuł tworzących

program P. Cel G ma postać

((B

 ....  B

))

  (B

 ...  B

) Zatem formuła

x

...

x

 ...  B

) wynika logicznie z P,

gdzie x

..., x

są wszystkimi zmiennymi występującymi w G. Tym samym znajdziemy wszystkie obiekty x

... x

spełniające cel G.

22. Podaj regułę rezolucji liniowej i derywacji liniowej.

Rezolucja liniowa:
<- A

, ..., A

- cel G

B <- B

, …, B

- wariant klauzuli C programu P

--------------------------
<-(A

, ..., A

m-1

, B

, ..., B

, A

m+1

, ..., A

)

 - nowy cel.

gdzie

 jest MGU zbioru {A

, B}, tzn. A

 = B

Derywacją liniową: dla P

 {G} nazywamy skończony lub nieskończony ciąg, którego wyrazami są (G

, C



), 1 <= n <= p lub 1

<= n, spełniający warunki:

a) dla każdego n, C

jest wariantem klauzuli programu P nie zawierającym zmiennych nie występujących w G

, G

, ..., G

n-1

b) dla każdego n, G

jest rezolucją liniową celu G

n-1

oraz klauzuli C

otrzymaną za pomocą podstawienia



23. Podaj określenie refutacji liniowej dla programu P i celu G oraz odpowiedzi obliczonej.

Refutacją liniową dla P

 {G} nazywamy skończoną liniową derywację dla P  {G}, której ostatni cel jest klauzulą pustą.

Odpowiedź obliczeniowa to podstawienie



...



ograniczone do zmiennych w G(



...



)|V(G) gdzie (G

, C



) jest refutacją

liniową dla P

 {G}

24. Podaj określenie odpowiedzi obliczonej i poprawnej dla P

{G}, gdzie P jest programem definitywnym, a G – celem. Sformułuj

twierdzenie o poprawności rezolucji liniowej.

Def. Niech



. . .



będą wszystkimi podstawieniami pewnej refutacji na gruncie P

 {G}.

Odpowiedzią obliczoną dla P

 {G} przez tę refutację nazywamy podstawieniem.

(



, ... ,



) | V(G).

Przykład
Ilustracja: x+y = z
Język: 0-stała; s-symbol następnika; (0,s(0), s(s(0))) - termy
sum(X,Y,Z) sens: X+Y=Z
program realizujący tą relację może wyglądać następująco:
klauzula jedn: /* 1 */ sum(X,0,X)



 = :- prolog/

reguła:

/* 2 */ sum(X,s(Y),s(Z))

 sum(X,Y,Z)

sum(s(0),s(0),Z ) - cel

: sum (X

,s(Y

),s(Z

))

 sum(X

)



= {X

/s(0),Y

/0,Z/s(Z

)}



 sum(s(0),s(0),s(Z

))



1 :

sum(s(0),s(0),s(Z

))

 sum(s(0),0,Z

)

sum(s(0),0,Z

) – cel drugi

: sum(X

,0,X

)





= {X

/s(0),Z

/s(0)}



 sum(s(0),0,s(0))



: sum(s(0),0,s(0))



Odpowiedź obliczona:
(



) | V(G) = {X

/s(0),Y

/0,Z/s(Z

)} {X

/s(0),Z

/s(0)} = { X

/s(0),Y

/0,Z/s(s(0)); X

/s(0),Z

/s(0) }

ograniczamy do V(G) = Z(



) czyli {Z/s(s(0))} lub {Z/ss(0)}

Tw. (o zgodności)
Każda odpowiedź obliczona dla pewnych G jest odpowiedzią poprawną dla P

{G}

W logice 1-rzędu zachodzą warunki:
A ╞

LPR

 A - dowolna formuła, nie ma kolizji zmiennych przy podstawieniach

A(x

,...,x

) ╞

LPR

A(t

,...,t

) x

, ... ,x

/ t

Wynika z prawa logiki pierwszego rzędu

 xA A[x/t]
Jeżeli A jest klauzulą to tak jest dla każdego podstawienia

.

25. Podaj określenie odpowiedzi obliczonej i poprawnej dla P

{G}, gdzie P jest programem definitywnym, a G – celem. Sformułuj

silne twierdzenie o pełności rezolucji liniowej.

Patrz pytanie 24 plus to co poniżej

Tw. 3 (o pełności rezolucji liniowej)

//nie wiem czy to jest silne tw.?

Jeżeli

 jest odpowiedzią poprawną dla P  { G}, to istnieje odpowiedź obliczona  dla P  { G} oraz podstawienie , takie, że G

  

Zanim udowodnimy twierdzenie 3:
G = ( A

A

,...,A

) to

 jest odpowiedzią poprawną dla P  { G} /cel programu P/,

gdy z P wynika na:



P ╞

LPR

1 Λ

...

)



 { G}

 że istnieją
P╞

LPR

 (A

1 Λ

...

)

(odp. poprawna - daje rozwiązania, że te elementy mogą spełniać)
(odp. obliczona generuje odpowiedzi poprawne)
Odp. poprawna powstaje z odpowiedzi obliczonej przez dalsze podstawianie. Z tego wynika, że musi istnieć refutacja, bo istnieje
odpowiedź.

26. Dla danego prog. definitywnego P podaj określenie uniwersum Herbranda, bazy Herbranda oraz zbioru sukcesów programu P.

L - ustalony język zawiera choć jedną stałą przedmiotową

Def. Zbiór wszystkich ustalonych termów języka L nazywamy uniwersum Herbranda dla L i oznaczamy U

Def. Strukturę M dla L nazywamy strukturą Herbranda jeżeli spełnione są warunki:

a) D

= U

– uniwersum struktury M

b) a

= a dla każdej stałej przedmiotowej

c) f

, .... , t

) = f (t

, .... , t

) dla każdego n-argumentowego symbolu funkcyjnego f oraz termów t

, ... , t

 U

Struktura – można traktować jako uproszczony rodzaj klas.( N(nazwa str.) O

... O

(zmienne) )

Def. Bazą Herbranda dla języka L nazywamy zbiór wszystkich zdań atomowych (atomów ustalonych) języka L. Oznaczamy
B

M - jakakolwiek struktura dla L
P ( t

, ... , t

) - zdanie atomowe

Definicja (dla wszelkich struktur)
M ╞ P ( t

, ... , t

)

 P

( t

, ... , t

)

Definicja dla M jako struktury Herbranda
M ╞ P ( t

, ... , t

)

P

( t

, ... , t

)

= { ( t

, ... , t

) M ╞ P ( t

, ... , t

) }

Przyjmujemy M = {A: M╞ A i A jest zdaniem atomowym }
M

 B

P - program definitywny
L

- język wyznaczony przez symbole pozalogiczne występujące w P

= U

= B

Program dla sum
U

= { 0, S(0), S(S(0)), ... } B

= { sum (t

, t

) : t

, t

 U

}

Def. Zbiór sukcesów programu
Zbiorem sukcesów programu P nazywamy zbiór:
S

= {A

B

: P

 {<-A} ma refutację liniową }

Inaczej: S

składa się z tych bazowych atomów A, dla których na pytanie A?(czy A zachodzi?) dostajemy odpowiedz obliczoną TAK.

27. Podaj określenie interpretacji Herbranda i modelu Herbranda dla programu P.

Def. Interpretacja Herbranda
Interpretacja Herbranda jest podzbiorem U

, np. zbiór wszystkich interpretacji Herbranda, ma postać:

Bp = { p(a), p(b), q(a), q(b), p(f(a)), p(f(b)), q(f(a)), … }

Def. Model Herbranda

Model Herbranda dla P to taka interpretacja Herbranda, będąca strukturą M taką, że M |= P

28. Podaj określenie zbioru sukcesów programu P, najmniejszego modelu Herbrandada P, oraz sformułuj słabe twierdzenie o

pełności rezolucji liniowej.

Def. Model Herbranda

Model Herbranda dla P to taka interpretacja Herbranda, będąca strukturą M taką, że M |= P

Tw1. M

jest najmniejszym modelem Herbranda dla P ( w sensie

)

Dowód:
Pokażemy, że dla każdego modelu Herbranda M╞ P mamy że M

 M.

Niech M ╞ P , M

 B

Niech A

 M

. Z definicji M

mamy, że P ╞

LPR

A skoro M ╞ P, to M ╞ A czyli A

M

Zatem (

A B

) (A

 M

 A M), a więc M

 M.

Wniosek:
A - atom ustalony to P ╞

LPR

M

╞ A

, ... , A

- atomy ustalone to P ╞

LPR

 ...  A

 M

╞ A

 ...  A

Symbole pozalogiczne języka programu otrzymują standardową interpretację w modelu M

Def. Zbiór sukcesów programu
Zbiorem sukcesów programu P nazywamy zbiór:
S

= {A

B

: P

 {<-A} ma refutację liniową }

Inaczej: S

składa się z tych bazowych atomów A, dla których na pytanie A?(czy A zachodzi?) dostajemy odpowiedz obliczoną TAK.

29. Podaj sposób konstrukcji modelu M

dla programu definitywnego P

BRAK DANYCH 

30. Podaj określenie SLD-drzewa, dla P

 {G} zgodnego z regułą selekcji R

SLD - Drzewo
Pojęcia:
Przyjmujemy: Program jest ciągiem klauzul.
P = (C

,..., C

)

w Prologu - liczy się kolejność klauzul.

Def.
SLD - drzewo dla P

 {G} zgodne z R to takie drzewo które:

G (cel) (

 A

, ..., A

, ... , A

)

... G

n-1

1,1

1,2

1, n2

...

Opis drzewa:
SLD drzewo - to drzewo skończone lub nieskończone, którego wierzchołki są etykietowane celami i spełnione są warunki:
a) korzeń jest etykietowany celem G
b) dla dowolnego wierzchołka etykietowanego celem G' następniki tego wierzchołka są etykietowane kolejnymi celami, które

powstają z G' przez uzgodnienie wybranego atomu (zgodnie z R) z kolejnymi klauzulami programu (pod warunkiem, że istnieją
takie klauzule programu ).

Gałąź - ciąg wierzchołków, że każde dwa sąsiednie są połączone krawędziami.
Gałęzie tego drzewa SLD pełnego reprezentują wszystkie derywacje dla P

 {G} zgodnie z R.

Gałęzie mogą być skończone lub nieskończone.
Gałęzie nieskończone - reprezentują nieskończoną derywacje (procedura się pętli)
c)   skończone gałęzie drzewa to:
a)                                                   b)


                                                            A

...., A ,..., A

refutacja                                             ..............................
(skończona pustą klauzulą)                  gałąź chybiona
(gałąź udana sukcesu)

Tylko 1-ne pełne drzewo (dokładnie jedno) rozwija tak długo jak się da. W tym drzewie się zawrą  wszystkie SLD (możliwe drogi).
Ma praktyczne znaczenie - cel znajdować te właściwe.

31.  Podaj określenie reguły selekcji i sformułuj twierdzenie o nieistotności reguł selskcji.

Reguła selekcji - metoda , procedura dowodzenia twierdzeń, ale to jeszcze nie algorytm.
Dwa "stopnie swobody" w rezolucji liniowej
 A

,...,A

, ...,A

– stopnie swobody

C = ( B

 B

,...,B

)

P C

–

klauzulę, którą będziemy unifikować

mamy A

 = B



 - MGU

Def. (nieformalna)
Reguła selekcji określa, który atom A

ma być wybrany na danym kroku (każdym kroku).

/ nieczuła na kontekst - łatwiejsza /
W praktyce najczęściej stosuje się regułę LEFT - FIRST (lewy najpierw) tzn. w celu

 A

,...,A

wybrany zawsze A

Def.
SLD - derywacją zgodną z regułą selekcji R nazywamy liniową derywację, w której na każdym kroku wybieramy atom zgodnie z R. /
nie musi kończyć się pustą klauzulą /
SLD - refutacja zgodna z R / musi kończyć się pustą klauzulą /
Tw. O nieistotności reguł selekcji
R

, R

- reguły selekcji

Jeżeli



jest odpowiedzią obliczoną dla P

 {G} zgodnie z R

, to istnieje odpowiedź obliczona



dla P

 {G} zgodnie z R

, taka że



jest wariantem G



Jeżeli weźmiemy 2 różne reguły selekcji, to zmienne odpowiedzi co najwyżej będą przemianowane:
G

A

,..., A

: A

...
G

 A

' A

/ Wyniki poprzednich dwóch rozdziałów zostaną zachowane, jeśli zachowają jakąkolwiek regułę selekcji  np. left – first /

32.  Podaj podstawowe cechy Prologu jako implementacji SLD rezolucji. Objaśnij użyte pojęcia.

Poszukiwanie gałęzi udanych w SLD - drzewie (reguła przeszukiwania)
Reguła przeszukiwania, poszukiwania (search rule) - metoda przeszukiwania SLD - drzewa (generowanie).
W praktyce stosuję się regułę "depth first" (najpierw w głąb) (przeszukujemy lewymi gałęziami). To znaczy (wcześniejsza reguła
selekcji) ustalamy, co unifikuje się z pierwszą możliwą klauzulą, którą można uzgodnić. Gdy doszliśmy do udanej idzie dalej, a gdy
dojdzie do chybionej to cofa się do tej, gdzie możliwy był wybór i dokonuje następnego wyboru. Tą metodę się wybiera - bo ją łatwo
jest realizować (pamięć programu stosu dostęp tylko do jednej na wierzchu). Porządek klauzul jest ważny w Prologu. Dla pewnych
drzew ta reguła może nie znaleźć rozwiązania. Dlatego też stosuje się inną reguła poszukiwania: "breadth-first" (najpierw wszerz).
Reguła jest bezpieczna wtedy, gdy znajdzie wszystkie udane gałęzie (postęp zgodnie z tą regułą). Ale ona jest bardzo
nieekonomiczna (obciąża pamięć i czas); w praktyce się jej nie stosuje.
W praktyce stosuje się regułę depth-first (PROLOG)
-

SLD – rezolucja; reguła selekcji i left first; reguła przeszukiwania: "depth-first"