Klauzulární logika. úvod. Šárka Vavrečková. 20. října Ústav informatiky Filozoficko-Přírodovědecká fakulta Slezské univerzity, Opava

Klauzulární logika — úvod —

Šárka Vavrečková Ústav informatiky Filozoficko-Přírodovědecká fakulta Slezské univerzity, Opava

20. října 2008

Úvod do klauzulární logiky

Syntaxe

Rezoluce

Univerzální tvrzení

Existenční tvrzení

Klauzulární logika Hlavní vlastnosti pracujeme s klauzulemi, které získáváme z klauzulí predikátové logiky klauzule klauzulární logiky: 1

2

3

ekvivalentními operacemi předsuneme postupně všechny kvantifikátory na začátek klauzule takto vytvořený prefix z kvantifikátorů odstraníme (ale při případných úpravách bereme v úvahu kvantifikaci jednotlivých proměnných a pořadí kvantifikátorů) jádro formule bez kvantifikátorů upravíme do klauzulární formy

používáme pouze jedinou logickou spojku – implikaci (žádnou jinou, ani negaci!), specifické vlastnosti nevyjádřitelné implikací reprezentujeme jinak


Syntaxe

Rezoluce




2

3




Syntaxe

Rezoluce




2

3




Syntaxe

Rezoluce




2

3




Syntaxe

Rezoluce




2

3




Syntaxe

Rezoluce




2

3




Syntaxe

Rezoluce



Definice klauzulí Definice (Klauzule) Báze: Literály predikátů jsou klauzule. Indukce: Jestliže A a B jsou klauzule, pak A - B je také klauzule. Zobecnění: Všechny formule, které jsou utvořeny použitím konečného počtu pravidel v bázi a indukci, jsou klauzule, žádná jiná formule není klauzule.


Syntaxe

Rezoluce



Definice klauzulí Definice (Hornovy klauzule) jsou klauzule s nejvýše jedním pozitivním literálem (tj. literálem bez negace). Můžeme je psát v následujících tvarech: A1 - A2 - . . . - An - B (A1 , A2 , . . . , An )

B

Definice ((Obecné) klauzule) A1 - A2 - . . . - An - B1 - B2 - Bm

(A1 &A2 & . . . &An )

(B1 - B2 - . . . - Bm )


Syntaxe

Rezoluce



Definice klauzulí Definice (Hornovy klauzule) jsou klauzule s nejvýše jedním pozitivním literálem (tj. literálem bez negace). Můžeme je psát v následujících tvarech: A1 - A2 - . . . - An - B (A1 , A2 , . . . , An )

B

Definice ((Obecné) klauzule) A1 - A2 - . . . - An - B1 - B2 - Bm

(A1 &A2 & . . . &An )

(B1 - B2 - . . . - Bm )


Syntaxe

Rezoluce



Abeceda 1

proměnné (X, Prom, . . . )

2

individuové konstanty (28, 3.4, jaguár, . . . )

3

logické konstanty (true, false – T, F)

4

existenční (Skolemovy) konstanty (@a, @něco,. . . )

5

funkční symboly (funktory) – mají přiřazenu aritu = přirozené číslo (vč. nuly) = počet argumentů

6

existenční (Skolemovy) funktory (@f,. . . ) – mají aritu

7

predikátové symboly – začínají písmenem, mají aritu

8

pomocné symboly – čárky, závorky

9

logická spojka implikace


Syntaxe

Rezoluce


Syntaktické prvky Term: proměnná konstanta (individuová, logická) existenční konstanta funktor, jehož argumenty jsou termy existenční funktor, jehož argumenty jsou termy

Atom: predikátový symbol, jehož argumenty jsou termy logická konstanta



Syntaxe

Rezoluce


Syntaktické prvky Term: proměnná konstanta (individuová, logická) existenční konstanta funktor, jehož argumenty jsou termy existenční funktor, jehož argumenty jsou termy

Atom: predikátový symbol, jehož argumenty jsou termy logická konstanta



Syntaxe

Rezoluce


Syntaktické prvky Klauzule: p1 , p2 , . . . , pn ´¹¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¸ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹¶

q1 , q2 , . . . , qm ´¹¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¸¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¶

antecedent(A)−konjunkce

konsekvent(K)−disjunkce

kde pi , qj jsou atomy.

Význam: (p1 &p2 & . . . &pn )

(q1 - q2 - . . . - qm )

(p1 &p2 & . . . &pn )

-

(q1 - q2 - . . . - qm )

p1 - p 2 - . . . - p n - q 1

-

q2 - . . . - qm



Syntaxe

Rezoluce


Syntaktické prvky Klauzule: p1 , p2 , . . . , pn ´¹¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¸ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹¶

q1 , q2 , . . . , qm ´¹¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¸¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¹ ¶

antecedent(A)−konjunkce

konsekvent(K)−disjunkce

kde pi , qj jsou atomy.

Význam: (p1 &p2 & . . . &pn )

(q1 - q2 - . . . - qm )

(p1 &p2 & . . . &pn )

-

(q1 - q2 - . . . - qm )

p1 - p 2 - . . . - p n - q 1

-

q2 - . . . - qm



Syntaxe

Rezoluce



Formy klauzulí Syntaxe p1 , p2 , . . . pn p1 , p2 , . . . pn

q1 , q2 , . . . qm q1 , q2 , . . . qm

Význam 1

žádná z množin A, K není prázdná (základní forma),

2

A=g

3

K = g NEPLATNÉ tvrzení.

je FAKT,

(1) (2) (3)


Syntaxe

Rezoluce


Rezoluce v klauzulární logice Odvození vzorce: p - X, X - q

à

p-q

p

à

p

X, X

q

q

substituce [A~ p], [B~q] A

X, X

B

à

A

B



Syntaxe

Rezoluce



à

p-q

p

à

p

X, X

q

q


X, X

B

à

A

B



Syntaxe

Rezoluce



à

p-q

p

à

p

X, X

q

q


X, X

B

à

A

B



Syntaxe

Rezoluce



Typy tvrzení Tvrzení jsou univerzální (tvrzení platí obecně pro vše, co je dosazeno), může obsahovat pouze univerzálně vázané proměnné (X, P rom, N ekdo, apod.), konstanty.

existenční (existuje hodnota taková, že po dosazení bude formule splněna), může obsahovat vše z předchozího bodu, existenční konstanty, existenční funktory.


Syntaxe

Rezoluce



Typy tvrzení Tvrzení jsou univerzální (tvrzení platí obecně pro vše, co je dosazeno), může obsahovat pouze univerzálně vázané proměnné (X, P rom, N ekdo, apod.), konstanty.

existenční (existuje hodnota taková, že po dosazení bude formule splněna), může obsahovat vše z předchozího bodu, existenční konstanty, existenční funktory.


Syntaxe

Rezoluce



Příklad Slovně „V létě mají všichni školáci prázdniny.ÿ

Predikátová logika v klauzulárním tvaru (chceme, aby každá proměnná byla vázaná obecným kvantifikátorem): ∀x rocni obd(leto) , skolak(x))

ma(x, prazdniny)

Klauzulární logika: rocni obd(leto), skolak(X)

ma(X, prazdniny)


Syntaxe

Rezoluce





ma(x, prazdniny)


ma(X, prazdniny)


Syntaxe

Rezoluce





ma(x, prazdniny)


ma(X, prazdniny)


Syntaxe

Rezoluce


Příklad Slovně „Psi štěkají (všichni psi štěkají, každý pes štěká).ÿ

Predikátová logika v klauzulárním tvaru ∀xpes(X)

steka(X)

Klauzulární logika: pes(X)

steka(X)



Syntaxe

Rezoluce




steka(X)


steka(X)



Syntaxe

Rezoluce




steka(X)


steka(X)



Syntaxe

Rezoluce



Příklad Slovně „V létě má listí zelenou barvu, zatímco na podzim má listí žlutou nebo červenou barvu.ÿ

Predikátová logika v klauzulárním tvaru ∀xrocni obd(leto) & listi(X) rocni obd(podzim) & listi(X)

barva(X, zelena) & barva(X, zluta) - barva(X, cervena)

Klauzulární logika: rocni obd(leto), listi(X) rocni obd(podzim), listi(X)

barva(X, zelena) barva(X, zluta), barva(X, cervena)


Syntaxe

Rezoluce









Syntaxe

Rezoluce









Syntaxe

Rezoluce


Příklad Slovně „Stůl je tvrdý.ÿ

Predikátová logika v klauzulárním tvaru ∀Xstul(X)

tvrdy(X)

stul(X)

tvrdy(X)

Klauzulární logika:

nebo

tvrdy(stul)



Syntaxe

Rezoluce




tvrdy(X)

stul(X)

tvrdy(X)


nebo

tvrdy(stul)



Syntaxe

Rezoluce




tvrdy(X)

stul(X)

tvrdy(X)


nebo

tvrdy(stul)



Syntaxe

Rezoluce


Příklad Slovně „Když je hezké počasí, děti jdou na procházku.ÿ

Predikátová logika v klauzulárním tvaru ∀Xpocasi(hezke) & dite(X)

jde(X, prochazka)

Klauzulární logika: pocasi(hezke), dite(X)

jde(X, prochazka)



Syntaxe

Rezoluce




jde(X, prochazka)


jde(X, prochazka)



Syntaxe

Rezoluce




jde(X, prochazka)


jde(X, prochazka)



Syntaxe

Rezoluce



Příklad Slovně „Musím do školy, protože píšu písemku.ÿ

Predikátová logika v klauzulárním tvaru pise(ja, pisemka)

musi do(ja, skola)

Klauzulární logika: pise(ja, pisemka) nebo ja(X), pise(X, pisemka)

musi do(ja, skola) musi do(X, skola)


Syntaxe

Rezoluce





musi do(ja, skola)




Syntaxe

Rezoluce





musi do(ja, skola)




Syntaxe

Rezoluce



Příklad Slovně „Děti mladší 10 let půjdou po zelené značce, děti starší půjdou po stejné značce jako dospělí.ÿ

Predikátová logika v klauzulárním tvaru ∀X dite(X) & vek(X) < 10

jde po(X, zelena)

∀X∀Y ∀Z dite(X) & vek(X) A= 10 & & dospely(Y ), jde po(Y, Z)

jde po(X, Z)

Klauzulární logika: dite(X), vek(X) < 10

jde po(X, zelena)

dite(X), vek(X) A= 10, dospely(Y ), jde po(Y, Z)

jde po(X, Z)


Syntaxe

Rezoluce





jde po(X, zelena)


jde po(X, Z)


jde po(X, zelena)


jde po(X, Z)


Syntaxe

Rezoluce





jde po(X, zelena)


jde po(X, Z)


jde po(X, zelena)


jde po(X, Z)


Syntaxe

Rezoluce


Převod z predikátové logiky

∃x

∀y

∀z

A(x,y,z)

A(@X, Y, Z)

∀x

∀y

∃z

A(x,y,z)

A(X, Y, @Z(X, Y ))

∀x

∃y

∀z

A(x,y,z)

A(X, @Y (X), Z)



Syntaxe

Rezoluce


Převod z predikátové logiky Existenční vazba

∃x

∀y

∀z

Existenční vazba

A(x,y,z)

Univerzální vazby

A(@X, Y, Z) Existenční vazba

∀x

∀y

∃z

A(x,y,z)

Univerzální vazby

A(X, Y, @Z(X, Y ))

∀x

∃y

∀z

A(x,y,z)

Univerzální vazby

A(X, @Y (X), Z)



Syntaxe

Rezoluce


Převod z predikátové logiky Existenční vazba

∃x

∀y

∀z

Existenční vazba

A(x,y,z)

Univerzální vazby

A(@X, Y, Z) Existenční vazba

∀x

∀y

∃z

A(x,y,z)

Univerzální vazby

A(X, Y, @Z(X, Y ))

∀x

∃y

∀z

A(x,y,z)

Univerzální vazby

A(X, @Y (X), Z)



Syntaxe

Rezoluce


Existenční konstanty Příklady 1

Jana něco vlastní (existuje něco, co vlastní Jana). vlastni(jana, @neco)

2

Někdo jde lesem. jde kudy(@nekdo, les)

3

Existuje někdo, koho baví logika (někoho baví logika). bavi(@nekdo, logika)

4

Vidím něco modrého. modre(@c)

vidi(ja, @c)



Syntaxe

Rezoluce




2


3


4


vidi(ja, @c)



Syntaxe

Rezoluce




2


3


4


vidi(ja, @c)



Syntaxe

Rezoluce




2


3


4


vidi(ja, @c)



Syntaxe

Rezoluce




2


3


4


vidi(ja, @c)



Syntaxe

Rezoluce


Existenční funktory Kdy použít existenční funktor „Každý zaměstnanec má svého nadřízeného.ÿ



Syntaxe

Rezoluce



Existenční funktory Kdy použít existenční funktor „Každý zaměstnanec má svého nadřízeného.ÿ Špatně: zamestnanec(X)

nadrizeny(Y, X)

(1)

zamestnanec(X)

nadrizeny(@c, X)

(2)


Syntaxe

Rezoluce



Existenční funktory Kdy použít existenční funktor „Každý zaměstnanec má svého nadřízeného.ÿ Špatně: zamestnanec(X)

nadrizeny(Y, X)

(1)

zamestnanec(X)

nadrizeny(@c, X)

(2)

Ve skutečnosti znamená: 1

Každý zaměstnanec má nadřízeného, který je v proměnné Y (tj. všichni jsou nadřízenými všech zaměstnanců).

2

Existuje nadřízený společný všem zaměstnancům.


Syntaxe

Rezoluce



Existenční funktory Kdy použít existenční funktor „Každý zaměstnanec má svého nadřízeného.ÿ Dobře: zamestnanec(X)

nadrizeny(@zam(X), X)

Každého nadřízeného vážeme vždy na konkrétního zaměstnance, existenční funktor @zam(X) je interpretován tabulkou.

Klauzulární logika. úvod. Šárka Vavrečková. 20. října Ústav informatiky Filozoficko-Přírodovědecká fakulta Slezské univerzity, Opava

Recommend Documents