AP14 Predikátová logika prvního řádu
Zadání
(syntax, sémantika, prenexace, skolemizace, unifikace, rezoluce)
Vypracování
Syntax
Predikát (značíme velkými písmeny, např. predikáty ) je n-ární relace; vyjadřuje vlastnosti objektů a vztahy mezi objekty.
unární predikáty vyjadřují vlastnosti
binární, ternární, …, n-ární vyjadřují vztahy mezi dvojicemi, trojicemi, …, n-ticemi objektů.
nulární predikáty (sentence) představují původní výroky ve výrokové logice (bez vypuštěných výrazů)
Konstanty (značíme ) reprezentují jména objektů; jedná se o prvky předem specifikované množiny hodnot D – domény
Proměnné (značíme ) zastupují jména objektů, mohou nabývat libovolných hodnot z dané domény
Funkce (značíme ) reprezentují složená jména objektů,
Příklad1)
Nechť funkce
reprezentují sčítání. Pak
(stejně jako
,
) jsou možná složená jména pro konstantu 3.
Termy jsou výrazy složené pouze z funkčních symbolů, konstant a proměnných
každá proměnná a každá konstanta je term
je-li
n-ární funkční symbol a
jsou termy, pak
je term
nic jiného není term
příklad termu:
Atomická formule
je-li
n-ární predikátový symbol a
jsou termy, pak
je atomická formule
jsou-li
a
termy, pak
je atomická formule
nic jiného není atomická formule
Je to tedy vlastně také predikát, ale často se uvádí zvlášť.
Formule jsou výrazy složené pouze z funkčních symbolů, konstant a proměnných
každá atomická formule je formule
je-li
formule, pak
je formule
jsou-li
formule, pak
jsou formule
je-li
proměnná a
formule, pak
a
jsou formule
nic jiného není formule
Podformule formule je libovolná spojitá podčást , která je sama formulí.
Příklad podformule3)
Formule
má kromě sebe samé následující podformule:
,
,
,
Vázaný/volný výskyt
výskyt proměnné
ve formuli
je
vázaný, pokud existuje podformule
formule
, která obsahuje tento výskyt
a začíná
, resp.
výskyt proměnné je
volný, není-li vázaný
4)
Výskyt proměné
z formule
předchozího příkladu je vázaný (podformulí je celá formule
), proměnné
a
jsou volné.
Sentence (uzavřená formule) – formule bez volných výskytů proměnných (všechny výskyty všech proměnných jsou vázané)
Otevřená formule – formule bez kvantifikátorů
Substituce – substituovat lze pouze volné proměnné.
Příklad substituce5)
Ve formuli:
lze provést například následující substituce.
substituce:
(
) =
,
(
) =
,
(
) =
nelze!:
(
) =
– došlo by k nežádoucí vazbě proměnných
Sématika
Interpretace (realizace) jazyka predikátové logiky je struktura složená z
libovolné neprázdné množiny
(domény, oboru interpretace)
zobrazení
pro každý
n-ární funkční symbol
n-ární relace
pro každý
n-ární predikátový symbol
,
Příklad6)
= celá čísla
,
(nulární funkce)
(funkce zadaná pomocí rovnosti funkcí: zobrazení
definujeme jako funkci sčítání celých čísel; pak např.
)
(relace zadaná pomocí rovnosti relací: definujeme jako relaci „větší než“ pro celá čísla; např. a )
Neformálně řečeno, interpretace je přiřazení konkrétních významů všem konstantám, funkčním a predikátovým symbolům.
Valuace – Interpretace volných proměnných spočívá v jejich ohodnocení, což je libovolné zobrazení (valuace) z množiny všech proměnných do . Neformálně řečeno, přiřazení konkrétních hodnot proměnným.
značí ohodnocení, které přiřazuje proměnné
prvek
a na ostatních proměnných splývá s valuací
Hodnota termu v interpretaci a valuaci je prvek z takový že:
je-li
proměnná,
je-li
, pak
je hodnotou funkce
pro argumenty
Příklad7)
Mějme interpretaci
z předchozího příkladu (celá čísla s > a +) a valuaci
. Pak
Pravdivost formulí
Formuli
nazveme pravdivou v interpretací
, je-li splňována
pro libovolnou valuaci; píšeme
Formule
je
tautologie, pokud je pravdivá pro každou interpretaci
splnitelná, pokud je pravdivá pro alespoň jednu interpretaci a valuaci.
kontradikce, pokud
je tautologie
Prenexace
Cílem Prenexové normální formy je převést libovolnou (uzavřenou) formuli do tvaru, v němž jsou všechny kvantifikátory na začátku a následuje otevřené (= bez kvantifikátorů) jádro v KNF (DNF).
Algoritmus převodu
eliminovat zbytečné kvantifikátory
přejmenovat proměnné tak, aby u každého kvantifikátoru byla jiná proměnná
eliminovat všechny spojky různé od
,
a
přesunout negaci dovnitř
přesunout kvantifikátory doleva
použít distributivní zákony k převodu jádra do KNF (DNF)
Skolemizace
Skolemova normální forma je prenexová normální forma s pouze univerzálními kvantifikátory.
odstraníme existenční (
) kvantifikátory
formuli
převedeme na
Algoritmus převodu
převést formuli do (konjunktivní) pnf
provést Skolemizaci: odstranit všechny existenční kvantifikátory a nahradit jimi vázané proměnné pomocnými Skolemovými funkcemi
Unifikace
směřuje k rezoluci v predikátové logice
formule uvádíme ve Skolemově normální formě
všeobecné kvantifikátory nepíšeme
problém se substitucemi proměnných obecně řeší unifikace
Konečná substituce je konečná množina , kde všechna jsou vzájemně různé proměnné a každé je term různý od .
pokud jsou všechna
uzavřené termy (neobsahují proměnné), jedná se o
uzavřenou substituci
pokud jsou
proměnné, označujeme
jako
přejmenování proměnných
Konečná substituce
označme libovolný term nebo literál jako výraz
je pak výsledek nahrazení všech výskytů všech
odpovídajícími termy
!POZOR! Nahrazení v rámci jedné substituce
probíhají paralelně. Když se použijí dvě substituce
, probíhají postupně.
Kompozice substitucí – postupně bereme prvky z první substituce a hledáme ve druhé, zda není možnost nahradit nahrazovaného (tranzitivně)
Unifikátor
Substituci nazveme unifikátorem množiny formulí , pokud , tedy v případě, že má jeden prvek.
Unifikátor množiny je nejobecnějším unifikátorem (mgu) , pokud pro libovolný unifikátor množiny existuje substituce taková, že – pro unifikovatelné množiny existuje pouze jediný mgu (až na přejmenování proměnných)
Rozdíly mezi výrazy označujeme jako
Mějme množinu výrazů S. Najdeme první (nejlevější) pozici, na které nemají všechny prvky S stejný symbol. Rozdíl D(S) mezi výrazy pak definujeme jako množinu podvýrazů všech
začínajících na této pozici.
8)
Unifikační algoritmus pro množinu výrazů S
krok 0:
,
krok k+1:
je-li
jednoprvková, ukonči algoritmus s výsledkem
jinak, pokud v
není proměnná v a term t, který ji neobsahuje, ukonči algoritmus s výsledkem neexistuje
jinak vyber takovou proměnnou v a term t, který neobsahuje v,
,
a pokračuj krokem k+2
Na pochopení fungování unifikačního algoritmu je dobré se podívat do skript Úvod do logiky a logického programování, na posledni stranu kapitoly
Predikátová logika III.
Rezoluce
Metoda vhodná pro strojové zpracování. Založená na vyvracení.
formule ve Skolemově normální formě, nepíšeme kvantifikátory
literály představují atomické formule a jejich negace
klauzule: množiny reprezentující disjunkci literálů
formule: množiny klauzulí reprezentující jejich konjunkci
Příklad rezoluční formule
formule:
rezoluční forma:
Rezoluční pravidlo pro predikátovou logiku. Mějme klauzule , bez společných proměnných (po případném přejmenování) ve tvaru:
-
.
Je-li
mgu množiny
, pak rezolventou
a
je
Příklad rezolventy
Rezolvujeme klauzule
a
mgu
aplikujeme mgu na
rezolventa
Vlastnosti rezoluce:
stejně jako ve výrokové logice je rezoluce v predikátové logice korektní a úplná
stejný problém jako ve výrokové logice: strategie generování rezolvent (příliš velký prohledávaný prostor)
lze použít všechny metody zjemnění uvedené pro výrokovou logiku
Druhy rezolucí:
Lineární rezoluce
LI-rezoluce
LD-rezoluce
SLD-rezoluce
Předměty
FI:IB101 Úvod do logiky a logického programování, doc. RNDr. Lubomír Popelínský, Ph.D.
Použitá literatura
Vypracoval
Martin Kotlík, UČO: 143208.
Otázku si přečetl pan RNDr. Jan Bouda a rámcově prošel. Jeho podněty pro doplnění textu, opravy nesrovnalostí a odstranění matoucích či k otázce se nevztahujících textů byly do otázky zaneseny. Tato kontrola je jen rámcová, stále se může stát, že v otázce zůstala zapomenutá chybka či nesrovnalost, vyučující za toto nenese odpovědnost, berte tuto rámcovou kontrolu jako formu pomoci od vyučujících pro studenty.