Teorie logického programování
Predikátová logika l.řádu
PROLOG: PROgramming in LOCic, část predikátové logiky l.řádu
■ fakta: rodic(petr, petri k), VXa(X)
■ klauzule: VX VY rodic(X,Y) => predek(X.Y) Predikátová logika I. řádu (PL1)
■ soubory objektů: lidé, čísla, body prostoru, ...
■ syntaxe PL1, sémantika PL1, pravdivost a dokazatelnost Rezoluce ve výrokové logice, v PL1
■ dokazovací metoda
Rezoluce v logickém programování Backtracking, řez, negace vs. rezoluce
Predikátová logika I. řádu (PL1)
Abeceda JA jazyka L PLI se skládá ze symbolů:
■ proměnné X, Y, ... označují libovolný objekt z daného oboru
■ funkční symboly f, g, ... označují operace (příklad: +, x )
■ arita = počet argumentů, n-ární symbol, značíme f/n
■ nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0,1,...)
■ predikátové symboly p,q, ... pro vyjádření vlastností a vztahů mezi objekty
■ arita = počet argumentů, n-ární symbol, značíme p/n      příklad: <, e
■ logické spojky a, v,     =>, =
■ kvantifikátory V, 3
■ logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu)
■ v logice 1. řádu nelze: v R : V A s R, V f : R -> R
■ závorky: ),(
Hana Rudová, Logické programování I, 19. března 2009 3 Predikátová logika
Hana Rudová, Logické programování I, 19. března 2009 2 Teorie logického programování
Jazyky PL1
■ Specifikace jazyka £ je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje
■ Jazyky s rovností: obsahují predikátový symbol pro rovnost „=" Příklady
■ jazyk teorie uspořádání
■ jazyk s =, binární prediátový symbol <
■ jazyk teorie množin
■ jazyk s =, binární predikátový symbol e
■ jazyk elementární aritmetiky
■ jazyk s =, nulární funkční symbol 0 pro nulu, unární funkční symbol s pro operaci následníka, binární funkční symboly pro sčítání + a násobení x
Hana Rudová, Logické programování I, 19. března 2009 4 Predikátová logika
Term, atomická formule, formule
Term nad abecedou JA
■ každá proměnná z JI je term
■ je-li f/n z JI a t\.....tn jsou termy, pak f(t\.....tn) je také term
■ každý term vznikne konečným počtem užití přechozích kroků f( X, g(X,0)) Atomická formule (atom) nad abecedou JA
■ je-li pln z    a ti.....tn jsou termy, pak p(t\.....tn) je atomická formule     f(X) < g(X,0)
Formule nad abecedou JA
■ každá atomická formule je formule
■ jsou-li F a G formule, pak také (-*F), (F a G), (F v G), (F => G), (F = G) jsou formule
■ je-li X proměnná a F formule, pak také (VX F) a (3X F) jsou formule
■ každá formule vznikne konečným počtem užití přechozích kroků     (3X ((f(X) = 0) a p(0)))
Hana Rudová, Logické programování I, 19. března 2009 5 Predikátová logika
Interpretace
■ Interpretace 1 jazyka L nad abecedou JA je dána
■ neprázdnou množinou T> (také značíme \1\, nazývá se univerzum) a
■ zobrazením, které
■ každé konstantě ceí přiřadí nějaký prvek T>
■ každému funkčnímu symbolu f/n e JA přiřadí n-ární operaci nad T>
■ každému predikátovému symbolu p In e JA přiřadí n-ární relaci nad T>
■ Příklad: uspořádání na R
■ jazyk: predikátový symbol mensí/2
■ interpretace: univerzum R; zobrazení: mensí(x,y) := x < y
■ Příklad: elementární aritmetika nad množinou N (včetně 0)
■ jazyk: konstanta zero, funční symboly s/l, plus/2
■ interpretace:
■ univerzum N; zobrazení: zero := 0,   s(x):=l+x,   plus(x,y) := x + y
Hana Rudová, Logické programování I, 19. března 2009 6 Predikátová logika
Sémantika formulí
Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu <p(r): každému termu je přiřazen prvek univerza
■ příklad: nechť <p(X) := 0
q>(plus(s(zero),X)) = cp(s(zero)) + cp(X) = (1 + cp(zero)) + 0= (1 + 0)+ 0=1
Každá dobře utvořená formule označuje pravdivostní hodnotu (pravda, nepravda) v závislosti na své struktuře a interpretaci Pravdivá formule 1 \=v Q: formule Q označena pravda Neravdivá formule 1 tyv Q: formule Q označena nepravda
■ příklad: p/1 predikátový symbol, tj. p s p := {(1), (3), (5>,...} '1 N p (zero) a p(s(zero)) iff '1 N p (zero) a 'i N p(s(zero))
iff  (qp(zero)) e p a (q?(s(zero))) e p iff  (qp(zero)) e p a <(1 + q?(zero)) e p iff <0)epa<l)ep (1) e p ale (0) é p, tedy formule je nepravdivá v '1
Hana Rudová, Logické programování I, 19. března 2009 7 Predikátová logika
Model
■ Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá
■ interpretace množiny N s obvyklými operacemi je modelem formule ( 1 + s(0) = s(s(0)))
■ interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule
■ Teorie T' jazyka £ je množina formulí jazyka £, tzv. axiomů
■ -i s(X) = Oje jeden z axiomů teorie elementární aritmetiky
■ Model teorie: libovolná interpretace, která je modelem všech jejích axiomů
■ všechny axiomy teorie musí být v této interpretaci pravdivé
■ Pravdivá formule v teorii T" f= F: pravdivá v každém z modelů teorie T"
■ říkáme také formule platí v teorii neboje splněna v teorii
■ formule 1 + s(0) = s(s(0))je pravdivá v teorii elementárních čísel
■ Logicky pravdivá formule f= F: libovolná interpretace je jejím modelem
■ nebo-li F je pravdivá v každém modelu libovolné teorie
■ formule C v    C je logicky pravdivá, formule 1 + s(0) = s(s(0)) není logicky pravdivá
Hana Rudová, Logické programování I, 19. března 2009 8 Predikátová logika
Zkoumání pravdivosti formulí
Korektnost a úplnost
Zjištění pravdivosti provádíme důkazem
Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka £, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích F j (j < í) použitím určitých odvozovacích pravidel
Odvozovací pravidla - příklady
■ pravidlo modus ponens: z formulí F a F => G lze odvodit G
■ rezoluční princip: z formulí F v A, G v -vl odvodit F v G
F je dokazatelná z formulí A\, ■ ■ ■ ,An A\, ■ ■ ■ ,An\- F
existuje-li důkaz F z A\, ■ ■ ■ ,An
Dokazatelné formule v teorii T" nazýváme teorémy teorie T"
Hana Rudová, Logické programování I, 19. března 2009 9 Predikátová logika
■ Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace)
■ VY ((0 < Y) a ( 3X (X < Y))) je uzavřená formule
■ ( 3X (X < Y) ) není uzavřená formule
■ Množina odvozovacích pravidel se nazývá korektní, jestliže pro každou množinu uzavřených formulí T a každou uzavřenou formuli F platí:
jestliže řhf pak T 1= F       (jestliže je něco dokazatelné, pak to platí)
Odvozovací pravidla jsou úplná, jestliže
jestliže T 1= F pak T V- F       (jestliže něco platí, pak je to dokazatelné)
■ PL1: úplná a korektní dokazatelnost, tj.
pro teorii T' s množinou axiomů JA platí: T' t= F právě když JA v- F
Hana Rudová, Logické programování I, 19. března 2009 10 Predikátová logika