3 Klauzuli celu: ∀x1

Denicja

Formuªa w postaci klauzulowej jest klauzul¡ hornowsk¡ lub programow¡, je±li jest uniwersalna: wszystkie zmienne w niej wyst¦puj¡ce s¡ zwi¡zane kwantykatorem uniwersalnym, a ka»da klauzula zawiera co najwy»ej jeden literaª pozytywny.

Klauzule hornowskie mog¡ wi¦c mie¢ nast¦puj¡cy ksztaªt:

1 Faktu: ∀_x1. . . ∀_xnr(t₁, . . . ,t_m), gdzie r jest symbolem relacji, t_i termami.

2 Reguªy: ∀_x1. . . ∀_xnq₁∧ . . . ∧q_m⇒q, gdzie q_i,q s¡ literaªami.

Literaª q jest postaci r(t₁, . . . ,t_m). Wtedy r nazywamy nagªówkiem reguªy lub faktu.

3 Klauzuli celu: ∀x1. . . ∀_xnq1∧ . . . ∧qm⇒, która jest logicznie równowa»na z ∀_x1. . . ∀_xn¬(q₁∧ . . . ∧q_m).

Denicja

Program logiczny to sko«czony zbiór faktów i reguª. Procedur¡

nazywamy podzbiór klauzul o tym samym nagªówku.

Przykªad 1. Rozwa»my nast¦puj¡cy program P:

{p(a, b), p(b, c), ∀x,y(p(x, y) ⇒ p(y, x)), ∀x,y,z((p(x, y)∧p(y, z)) ⇒ p(x, z))}

Šatwo si¦ domy±le¢, »e rozwa»amy j¦zyk ze staªymi {a, b, c} i symbolem relacji dwuargumentowej p. Podane s¡ pewne fakty i reguªy orzekaj¡ce, »e p jest symetryczna i przechodnia. Z ró»nych powodów takich, jak problemy implementacyjne, czy fakt, »e u»ywamy tylko kwantykatorów uniwersalnych, program ten w notacji stosowanej w Prologu ma posta¢:

p(a, b). (1)

p(b, c). (2)

p(A, B) : −p(A, C), p(C, B). (3) p(X , Y ) : −p(Y , X ). (4)

Zmienne oznaczane s¡ wielkimi literami, u»ywa si¦ spójnika : − ó ile ", a przecinek oznacza koniunkcj¦. Mo»na zawsze zapisa¢ reguªy tak, »e w ró»nych nie wyst¦puj¡ te same zmienne. Ten ostatni warunek nie jest konieczny. Zwykle system wnioskowania potra

sobie radzi¢ z powtórkami wyst¡pie«, dokonuj¡c wªasnego

oznaczania zmiennych. Wykonanie obliczenia podanego programu polega na podaniu klauzuli celu C np. : −p(a, c) i ustaleniu, czy zbiór P ∪ {C} jest sprzeczny. Odbywa si¦ to z wykorzystaniem rezolucji i chodzi wtedy o uzyskanie klauzuli pustej. W tym przypadku jest to bardzo proste: Bior¡c klauzul¦ celu i reguª¦ 3.

dokonujemy podstawienia A := a, B := c i stosuj¡c rezolucj¦

uzyskujemy klauzul¦ : −p(a, C), p(C, c)., która równie» jest klauzul¡ celu. Oznacza to, »e aby obali¢ twierdzenie p(a, c) wystarczy obali¢ ∃Cp(a, C), p(C, b)., bo aktualny cel jest jego negacj¡. W tym celu dokujemy postawienia C := b, stosujemy rezolucj¦ do faktu 1 i mamy klauzul¦ ; −p(b, c), która w sposób oczywisty jest sprzeczna z fatem 2, wi¦c otrzymujemu upragnion¡

klauzul¦ pust¡.

Rozwa»my program

p(X , Y ) : −p(Y , X ). (1)

p(a, b). (2)

p(b, c). (3)

p(A, B) : −p(A, C), p(C, B). (4)

który jest logicznie równowa»ny poprzedniemu. Okazuje si¦ jednak,

»e napisali±my pierwszy program logiczny, który si¦ p¦tli! Je±li podamy dowoln¡ klauzul¦ celu typu : −p(X , Y )., to poniewa»

rzeczywiste systemy generuj¡ dowód systematycznie analizuj¡c reguªy t.j. wedªug ich kolejno±ci w programie, cel ten b¦dzie zast¡piony : −p(Y , X )., a ten : −p(X , Y )., co nieuchronnie prowadzi to niepo»¡danej sytuacj

Denicja

Reguª¡ wyszukiwania nazywamy sposób wyboru klauzuli, która b¦dzie u»yta wraz z wybranym celem do wyprowadzenia rezolwenty.

Natomiast sposób wyboru literaªu nazywamy reguª¡ obliczeniow¡.

Wcze±niejszy przykªad pokazuje, »e zwykle obowi¡zuje zasada starsze«stwa: dla klauzuli celu wybiera si¦ literaª pierwszy z lewej, i wyszukuje pierwsz¡, reguª¦ w programie, która mo»e by¢ u»yta do wyprowadzenia rezolwenty. St¡d mamy denicj¦:

Denicja (SLD-rezolucj¡)

Niech P b¦dzie zbiorem klauzul programu, R reguª¡ obliczeniow¡, S reguª¡ wyszukiwania, a G klauzul¡ celu. SLD-wywodem

nazywamy sekwencj¦ kroków rezolucyjnych wykonywanych na rezolwentach i klauzulach programu, gdzie jako pierwsz¡ rezolwent¦

G0 przyjmuje si¦ klauzul¦ G. Klauzul¦ Gi+1 tworzymy przez wybór literaªu A_i ∈G_i zgodnie z reguª¡ obliczeniow¡ i wybór reguªy C_i programu P zgodnie z reguª¡ wyszykiwania, które mo»na uzgodni¢

dokonuj¡c podstawienia si i wykona¢ jeden krok rezolucji.

SLD-dowodem nazywamy wywód zako«czony klauzul¡ pust¡.

Przykªadowy program w Prologu

t(X , X ) : −atomic(X ).

t(X , Y ) : −X = ..[∗, Y 1, Y 2], Y 3 = ..[/, 1, Y 2], Y = ..[/, Y 1, Y 3].

d(x, x, 1) : −!.

d(C,,0) : −atomic(C).

d(−U, x, −A) : −d(U, x, A).

d(U + V , x, A + B) : −d(U, x, A), d(V , x, B).

d(U ∗ V , x, A ∗ V + U ∗ B) : −d(U, x, A), d(V , x, B).

d(U/V , x, A) : −d(U ∗ V⁻¹,x, A).

d(U^C,x, C ∗ U^C−1∗A) : −atomic(C), d(U, x, A).