Predikátová logika l.řádu Teorie logického programování -• PROLOG: PROgramming in LOGic, část predikátové logiky l.řádu -• fakta: rodic(petr,petrik), VXa(X) -• klauzule: VXVY rodic(X,Y) => predek(X,Y) Hana Rudová, Logické programování I, 31. března 2010 2 Teorie logického programování Teorie logického programování -• PROLOG: PROgramming in LOGic, část predikátové logiky l.řádu -• fakta: rodic(petr,petrik), VXa(X) -• klauzule: VXVY rodic(X,Y) => predek(X,Y) -• Predikátová logika I. řádu (PL1) 3 soubory objektů: lidé, čísla, body prostoru, ... M syntaxe PL1, sémantika PL1, pravdivost a dokazatelnost Hana Rudová, Logické programování I, 31. března 201 0 2 Teorie logického programování Teorie logického programování -• PROLOG: PROgramming in LOGic, část predikátové logiky l.řádu -• fakta: rodic(petr,petrik), VXa(X) -• klauzule: VXVY rodic(X,Y) => predek(X,Y) -• Predikátová logika I. řádu (PL1) 3 soubory objektů: lidé, čísla, body prostoru, ... M syntaxe PL1, sémantika PL1, pravdivost a dokazatelnost -• Rezoluce ve výrokové logice, v PL1 -• dokazovací metoda 3 Rezoluce v logickém programování -• Backtracking, řez, negace vs. rezoluce Hana Rudová, Logické programování I, 31. března 2010 2 Teorie logického programování Predikátová logika I. řádu (PL1) Abeceda JA jazyka £ PL1 se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru Hana Rudová, Logické programování I, 31. března 201 0 3 Predikátová logika Predikátová logika I. řádu (PLl) Abeceda JA jazyka £ PLl se skládá ze symbolů: -• proměnné X, Y, ... označují libovolný objekt z daného oboru M funkční symboly f, g, ... označují operace (příklad: +, x ) M 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, ...) Hana Rudová, Logické programování I, 31. března 201 0 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda JA jazyka £ PL1 se skládá ze symbolů: -• proměnné X, Y, ... označují libovolný objekt z daného oboru M funkční symboly f, g, ... označují operace (příklad: +, x ) M 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 M arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e Hana Rudová, Logické programování I, 31. března 201 0 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda JA jazyka £ PL1 se skládá ze symbolů: -• proměnné X, Y, ... označují libovolný objekt z daného oboru M funkční symboly f, g, ... označují operace (příklad: +, x ) M 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 M arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e -• logické spojky a, v, ->, =>, = Hana Rudová, Logické programování I, 31. března 201 0 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda JA jazyka £ PL1 se skládá ze symbolů: -• proměnné X, Y, ... označují libovolný objekt z daného oboru M funkční symboly f, g, ... označují operace (příklad: +, x ) M 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 M arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e -• logické spojky a, v, ->, =>, = -• kvantifikátory V, 3 M logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) M v logice 1. řádu nelze: v R : VA c R, y f : R - R Hana Rudová, Logické programování I, 31. března 201 0 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda JA jazyka £ PL1 se skládá ze symbolů: -• proměnné X, Y, ... označují libovolný objekt z daného oboru M funkční symboly f, g, ... označují operace (příklad: +, x ) M 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 M arita = počet argumentů, n-ární symbol, značíme p/n příklad: <, e -• logické spojky a, v, ->, =>, = -• kvantifikátory V, 3 M logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) M v logice 1. řádu nelze: v R : VA c R, y f : R - R M závorky: ),( Hana Rudová, Logické programování I, 31. března 2010 3 Predikátová logika Jazyky PLI -• Specifikace jazyka L je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje M Jazyky s rovností: obsahují predikátový symbol pro rovnost ,=" Hana Rudová, Logické programování I, 31. března 201 0 4 Predikátová logika Jazyky PLI -• Specifikace jazyka L je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje M Jazyky s rovností: obsahují predikátový symbol pro rovnost ,=" Příklady -• jazyk teorie uspořádání -• jazyk s =, binární prediátový symbol < Hana Rudová, Logické programování I, 31. března 201 0 4 Predikátová logika Jazyky PLI -• Specifikace jazyka L je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje M 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 3 jazyk s =, binární predikátový symbol e Hana Rudová, Logické programování I, 31. března 201 0 4 Predikátová logika Jazyky PLI -• Specifikace jazyka L je definována funkčními a predikátovými symboly symboly tedy určují oblast, kterou jazyk popisuje M 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 3 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, 31. března 2010 4 Predikátová logika Term, atomická formule, formule -• Term nad abecedou JA M každá proměnná z JA je term M je-li f/n z JA a ti,...,tn jsou termy, pak /(ti,..., tn) je také term <• každý term vznikne konečným počtem užití přechozích kroků f( X, g(X,0)) Hana Rudová, Logické programování I, 31. března 201 0 5 Predikátová logika Term, atomická formule, formule -• Term nad abecedou JA M každá proměnná z JA je term M je-li f In z JA a ti,..., tn jsou termy, pak /(ti,..., tn) je také term <• každý term vznikne konečným počtem užití přechozích kroků f( X, g(X,0)) M Atomická formule (atom) nad abecedou JA -• je-li p In z JA a ti,..., tn jsou termy, pak p(ti,...,tn) je atomická formule f(X) < g(X,0) Hana Rudová, Logické programování I, 31. března 201 0 5 Predikátová logika Term, atomická formule, formule -• Term nad abecedou JA M každá proměnná z JA je term M je-li f In z JA a ti,..., tn jsou termy, pak /(ti,..., tn) je také term <• každý term vznikne konečným počtem užití přechozích kroků f( X, g(X,0)) M Atomická formule (atom) nad abecedou JA 3 je-li pln z JA a ti,..., tn jsou termy, pak p(ti,...,tn) je atomická formule f(X) < g(X,0) -• Formule nad abecedou JA M každá atomická formule je formule -• jsou-li F a G formule, pak také OF), (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 3 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, 31. března 201 0 5 Predikátová logika Interpretace -• Interpretace 1 jazyka L nad abecedou JA je dána -• neprázdnou množinou V (také značíme \1\, nazývá se univerzum) a M zobrazením, které s* každé konstantě c g JA přiřadí nějaký prvek V ± každému funkčnímu symbolu f In g JA přiřadí n-ární operaci nad V ± každému predikátovému symbolu p/n g JA přiřadí n-ární relaci nad V Hana Rudová, Logické programování I, 31. března 201 0 6 Predikátová logika Interpretace -• Interpretace 1 jazyka L nad abecedou JA je dána -• neprázdnou množinou V (také značíme \1\, nazývá se univerzum) a M zobrazením, které s* každé konstantě c g JA přiřadí nějaký prvek V ± každému funkčnímu symbolu f In g JA přiřadí n-ární operaci nad V ± každému predikátovému symbolu p/n g JA přiřadí n-ární relaci nad V M Příklad: uspořádání na M 3 jazyk: predikátový symbol menšili 3 interpretace: univerzum R; zobrazení: mensí(x,y) := x < y Hana Rudová, Logické programování I, 31. března 201 0 6 Predikátová logika Interpretace -• Interpretace 1 jazyka L nad abecedou JA je dána -• neprázdnou množinou V (také značíme \1\, nazývá se univerzum) a M zobrazením, které s* každé konstantě c g JA přiřadí nějaký prvek V ± každému funkčnímu symbolu f In g JA přiřadí n-ární operaci nad V ± každému predikátovému symbolu p/n g JA přiřadí n-ární relaci nad V M Příklad: uspořádání na M 3 jazyk: predikátový symbol menšili 3 interpretace: univerzum R; zobrazení: mensí(x,y) := x < y M Příklad: elementární aritmetika nad množinou N (včetně 0) -• jazyk: konstanta zero, funční symboly 5/1, plus 12 M interpretace: ± univerzum N; zobrazení: zero := 0, s(x):=l+x, plus(x,y) := x + y Hana Rudová, Logické programování I, 31. března 2010 6 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1 M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1 M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + op(X) = Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1 M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + op(X) = (1 + qp(zero)) + 0 = Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 *0 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 N^ Q: formule Q označena pravda Neravdivá formule 1 ^m Q: formule Q označena nepravda Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 *0 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 N^ Q: formule Q označena pravda Neravdivá formule 1 ^ Q: formule Q označena nepravda M příklad: pII predikátový symbol, tj. p q lil p := {(1), (3), (5),...} 1 \= p (zero) a p (s (zero)) Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 *0 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 N^ Q: formule Q označena pravda Neravdivá formule 1 ^ Q: formule Q označena nepravda M příklad: pII predikátový symbol, tj. p q lil p := {(1), (3), (5),...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 *0 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 N^ Q: formule Q označena pravda Neravdivá formule 1 ^ Q: formule Q označena nepravda M příklad: pII predikátový symbol, tj. p q lil p := {(1), (3), (5),...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (op(zero)) g p a (op(s(zero))) g p Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 *0 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 N^ Q: formule Q označena pravda Neravdivá formule 1 ^ Q: formule Q označena nepravda M příklad: pII predikátový symbol, tj. p q lil p := {(1), (3), (5),...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (op(zero)) g p a (op(s(zero))) g p iff (op(zero)) g p a ((1 + qp(zero)} g p Hana Rudová, Logické programování I, 31. března 201 0 7 Predikátová logika Sémantika formulí -• Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ M Hodnota termu qp(t): každému termu je přiřazen prvek univerza -• příklad: nechť qp(X) := 0 qp (plus (s (zero), X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 *0 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 N^ Q: formule Q označena pravda Neravdivá formule 1 ^ Q: formule Q označena nepravda M příklad: pII predikátový symbol, tj. p q lil p := {(1), (3), (5),...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (op(zero)) g p a (op(s(zero))) g p iff (op(zero)) g p a ((1 + qp(zero)} g p iff {0)epa{l)ep {1} g p ale (0) é p, tedy formule je nepravdivá v 1 Hana Rudová, Logické programování I, 31. března 2010 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 Hana Rudová, Logické programování I, 31. března 2010 8 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 M Teorie CT jazyka L je množina formulí jazyka Ľ, tzv. axiomů M -■ s(X) = 0 je jeden z axiomů teorie elementární aritmetiky Hana Rudová, Logické programování I, 31. března 2010 8 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 M Teorie CT jazyka L je množina formulí jazyka Ľ, tzv. axiomů M -■ s(X) = 0 je jeden z axiomů teorie elementární aritmetiky -• Model teorie: libovolná interpretace, která je modelem všech jejích axiomů M všechny axiomy teorie musí být v této interpretaci pravdivé Hana Rudová, Logické programování I, 31. března 2010 8 Predikátová logika Model -• Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá 3 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 M Teorie CT jazyka L je množina formulí jazyka Ľ, tzv. axiomů 3 -■ s(X) = 0 je jeden z axiomů teorie elementární aritmetiky -• Model teorie: libovolná interpretace, která je modelem všech jejích axiomů M všechny axiomy teorie musí být v této interpretaci pravdivé M Pravdivá formule v teorii Ť \= F: pravdivá v každém z modelů teorie CT M říkáme také formule platí v teorii nebo je splněna v teorii 3 formule 1 + s(0) = s(s(0)) je pravdivá v teorii elementárních čísel Hana Rudová, Logické programování I, 31. března 201 0 8 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 M Teorie CT jazyka L je množina formulí jazyka Ľ, tzv. axiomů M -■ s(X) = 0 je jeden z axiomů teorie elementární aritmetiky -• Model teorie: libovolná interpretace, která je modelem všech jejích axiomů M všechny axiomy teorie musí být v této interpretaci pravdivé M Pravdivá formule v teorii Ť \= F: pravdivá v každém z modelů teorie CT M říkáme také formule platí v teorii nebo je splněna v teorii 3 formule 1 + s(0) = s(s(0)) je pravdivá v teorii elementárních čísel -• Logicky pravdivá formule i= F: libovolná interpretace je jejím modelem M nebo-li F je pravdivá v každém modelu libovolné teorie M formule G v -> G je logicky pravdivá, formule 1 + s(0) = s(s(0)) není logicky pravdivá Hana Rudová, Logické programování I, 31. března 2010 8 Predikátová logika Zkoumání pravdivosti formulí -• Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F\,..., 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 Hana Rudová, Logické programování I, 31. března 201 0 9 Predikátová logika Zkoumání pravdivosti formulí -• Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F\,..., 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 - príklady -• pravidlo modus ponens: z formulí F a F ^> G lze odvodit G Hana Rudová, Logické programování I, 31. března 201 0 9 Predikátová logika Zkoumání pravdivosti formulí -• Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F\,..., 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 - príklady -• pravidlo modus ponens: z formulí F a F ^> G lze odvodit G -• rezoluční princip: z formulí F v A, G v ~^A odvodit F v G Hana Rudová, Logické programování I, 31. března 201 0 9 Predikátová logika Zkoumání pravdivosti formulí -• Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fu-.., 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 - príklady -• pravidlo modus ponens: z formulí F a F ^> G lze odvodit G -• rezoluční princip: z formulí F v A, G v ~^A odvodit F v G M F je dokazatelná z formulí Au ■ ■ ■ ,An Au ■ ■ ■ ,An \- F existuje-li důkaz F z Au • • • ,An Hana Rudová, Logické programování I, 31. března 201 0 9 Predikátová logika Zkoumání pravdivosti formulí -• Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fu-.., 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 - príklady -• pravidlo modus ponens: z formulí F a F ^> G lze odvodit G 3 rezoluční princip: z formulí F v A, G v ~^A odvodit F v G M F je dokazatelná z formulí Au ■ ■ ■ ,An Au ■ ■ ■ ,An \- F existuje-li důkaz F z Au • • • ,An M Dokazatelné formule v teorii Ť nazýváme teorémy teorie Ť Hana Rudová, Logické programování I, 31. března 201 0 9 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) * VY ((0 < Y) a ( 3X (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule Hana Rudová, Logické programování I, 31. března 2010 10 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) * VY ((0 < Y) a ( 3X (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule M 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 T \- F pak T N F (jestliže je něco dokazatelné, pak to platí) Hana Rudová, Logické programování I, 31. března 201 0 1 0 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) * VY ((0 < Y) a ( 3X (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule M 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 T \- F pak T N F (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže T N F pak T \- F (jestliže něco platí, pak je to dokazatelné) Hana Rudová, Logické programování I, 31. března 201 0 1 0 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) * VY ((0 < Y) a ( 3X (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule M 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 T V- F pak T N F (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže T N F pak T V- F (jestliže něco platí, pak je to dokazatelné) M PLI: úplná a korektní dokazatelnost, tj. pro teorii CT s množinou axiomů JA platí: Ť \= F právě když JA \- F Hana Rudová, Logické programování I, 31. března 201 0 1 0 Predikátová logika