Predikátová logika 1.řádu Teorie logického programování PROLOG: PROgramming in LOGic, část predikátové logiky 1.řádu fakta: rodic(petr,petrik), X a(X) klauzule: X Y rodic(X,Y) predek(X,Y) Hana Rudová, Logické programování I, 18. března 2007 2 Teorie logického programování Teorie logického programování PROLOG: PROgramming in LOGic, část predikátové logiky 1.řádu fakta: rodic(petr,petrik), X a(X) klauzule: X Y 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 Hana Rudová, Logické programování I, 18. března 2007 2 Teorie logického programování Teorie logického programování PROLOG: PROgramming in LOGic, část predikátové logiky 1.řádu fakta: rodic(petr,petrik), X a(X) klauzule: X Y 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 Hana Rudová, Logické programování I, 18. března 2007 2 Teorie logického programování Predikátová logika I. řádu (PL1) Abeceda A jazyka L PL1 se skládá ze symbolů: proměnné X, Y, . . . označují libovolný objekt z daného oboru Hana Rudová, Logické programování I, 18. března 2007 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda A jazyka L PL1 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: +, × ) 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, 18. března 2007 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda A jazyka L PL1 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: +, × ) 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: <, Hana Rudová, Logické programování I, 18. března 2007 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda A jazyka L PL1 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: +, × ) 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: <, logické spojky , , , , Hana Rudová, Logické programování I, 18. března 2007 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda A jazyka L PL1 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: +, × ) 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: <, logické spojky , , , , kvantifikátory , logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) v logice 1. řádu nelze: v R : A R, f : R R Hana Rudová, Logické programování I, 18. března 2007 3 Predikátová logika Predikátová logika I. řádu (PL1) Abeceda A jazyka L PL1 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: +, × ) 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: <, logické spojky , , , , kvantifikátory , logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) v logice 1. řádu nelze: v R : A R, f : R R závorky: ),( Hana Rudová, Logické programování I, 18. března 2007 3 Predikátová logika Jazyky PL1 Specifikace jazyka L 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 ,,=" Hana Rudová, Logické programování I, 18. března 2007 4 Predikátová logika Jazyky PL1 Specifikace jazyka L 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 < Hana Rudová, Logické programování I, 18. března 2007 4 Predikátová logika Jazyky PL1 Specifikace jazyka L 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 Hana Rudová, Logické programování I, 18. března 2007 4 Predikátová logika Jazyky PL1 Specifikace jazyka L 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 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í × Hana Rudová, Logické programování I, 18. března 2007 4 Predikátová logika Term, atomická formule, formule Term nad abecedou A každá proměnná z A je term je-li f/n z A a t1, . . . , tn jsou termy, pak f(t1, . . . , 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, 18. března 2007 5 Predikátová logika Term, atomická formule, formule Term nad abecedou A každá proměnná z A je term je-li f/n z A a t1, . . . , tn jsou termy, pak f(t1, . . . , 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 A je-li p/n z A a t1, . . . , tn jsou termy, pak p(t1, . . . , tn) je atomická formule f(X) < g(X,0) Hana Rudová, Logické programování I, 18. března 2007 5 Predikátová logika Term, atomická formule, formule Term nad abecedou A každá proměnná z A je term je-li f/n z A a t1, . . . , tn jsou termy, pak f(t1, . . . , 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 A je-li p/n z A a t1, . . . , tn jsou termy, pak p(t1, . . . , tn) je atomická formule f(X) < g(X,0) Formule nad abecedou A každá atomická formule je formule jsou-li F a G formule, pak také (F), (F G), (F G), (F G), (F G) jsou formule je-li X proměnná a F formule, pak také (X F) a (X F) jsou formule každá formule vznikne konečným počtem užití přechozích kroků (X ((f(X) = 0) p(0))) Hana Rudová, Logické programování I, 18. března 2007 5 Predikátová logika Interpretace Interpretace I jazyka L nad abecedou A je dána neprázdnou množinou D (také značíme |I|, nazývá se univerzum) a zobrazením, které každé konstantě c A přiřadí nějaký prvek D každému funkčnímu symbolu f/n A přiřadí n-ární operaci nad D každému predikátovému symbolu p/n A přiřadí n-ární relaci nad D Hana Rudová, Logické programování I, 18. března 2007 6 Predikátová logika Interpretace Interpretace I jazyka L nad abecedou A je dána neprázdnou množinou D (také značíme |I|, nazývá se univerzum) a zobrazením, které každé konstantě c A přiřadí nějaký prvek D každému funkčnímu symbolu f/n A přiřadí n-ární operaci nad D každému predikátovému symbolu p/n A přiřadí n-ární relaci nad D Příklad: uspořádání na R jazyk: predikátový symbol mensi/2 interpretace: univerzum R; zobrazení: mensi(x, y) := x < y Hana Rudová, Logické programování I, 18. března 2007 6 Predikátová logika Interpretace Interpretace I jazyka L nad abecedou A je dána neprázdnou množinou D (také značíme |I|, nazývá se univerzum) a zobrazením, které každé konstantě c A přiřadí nějaký prvek D každému funkčnímu symbolu f/n A přiřadí n-ární operaci nad D každému predikátovému symbolu p/n A přiřadí n-ární relaci nad D Příklad: uspořádání na R jazyk: predikátový symbol mensi/2 interpretace: univerzum R; zobrazení: mensi(x, y) := x < y Příklad: elementární aritmetika nad množinou N (včetně 0) jazyk: konstanta zero, funční symboly s/1, plus/2 interpretace: univerzum N; zobrazení: zero := 0, s(x) := 1 + x, plus(x, y) := x + y Hana Rudová, Logické programování I, 18. března 2007 6 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (zero)) + 0 = Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (zero)) + 0 = (1 + 0) + 0 = 1 Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (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 I Q: formule Q označena PRAVDA Neravdivá formule I Q: formule Q označena NEPRAVDA Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (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 I Q: formule Q označena PRAVDA Neravdivá formule I Q: formule Q označena NEPRAVDA příklad: p/1 predikátový symbol, tj. p |I| p := { 1 , 3 , 5 , . . .} I p(zero) p(s(zero)) Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (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 I Q: formule Q označena PRAVDA Neravdivá formule I Q: formule Q označena NEPRAVDA příklad: p/1 predikátový symbol, tj. p |I| p := { 1 , 3 , 5 , . . .} I p(zero) p(s(zero)) iff I p(zero) a I p(s(zero)) Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (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 I Q: formule Q označena PRAVDA Neravdivá formule I Q: formule Q označena NEPRAVDA příklad: p/1 predikátový symbol, tj. p |I| p := { 1 , 3 , 5 , . . .} I p(zero) p(s(zero)) iff I p(zero) a I p(s(zero)) iff (zero) p a (s(zero)) p Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (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 I Q: formule Q označena PRAVDA Neravdivá formule I Q: formule Q označena NEPRAVDA příklad: p/1 predikátový symbol, tj. p |I| p := { 1 , 3 , 5 , . . .} I p(zero) p(s(zero)) iff I p(zero) a I p(s(zero)) iff (zero) p a (s(zero)) p iff (zero) p a (1 + (zero) p Hana Rudová, Logické programování I, 18. března 2007 7 Predikátová logika Sémantika formulí Ohodnocení proměnné (X): každé proměnné X je přiřazen prvek |I| Hodnota termu (t): každému termu je přiřazen prvek univerza příklad: necht' (X) := 0 (plus(s(zero), X)) = (s(zero)) + (X) = (1 + (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 I Q: formule Q označena PRAVDA Neravdivá formule I Q: formule Q označena NEPRAVDA příklad: p/1 predikátový symbol, tj. p |I| p := { 1 , 3 , 5 , . . .} I p(zero) p(s(zero)) iff I p(zero) a I p(s(zero)) iff (zero) p a (s(zero)) p iff (zero) p a (1 + (zero) p iff 0 p a 1 p 1 p ale 0 p, tedy formule je nepravdivá v I Hana Rudová, Logické programování I, 18. března 2007 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/1: s(x):=x není modelem této formule Hana Rudová, Logické programování I, 18. března 2007 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/1: s(x):=x není modelem této formule Teorie T jazyka L je množina formulí jazyka L, tzv. axiomů s(X) = 0 je jeden z axiomů teorie elementární aritmetiky Hana Rudová, Logické programování I, 18. března 2007 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/1: s(x):=x není modelem této formule Teorie T jazyka L je množina formulí jazyka L, tzv. axiomů s(X) = 0 je 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é Hana Rudová, Logické programování I, 18. března 2007 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/1: s(x):=x není modelem této formule Teorie T jazyka L je množina formulí jazyka L, tzv. axiomů s(X) = 0 je 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: pravdivá v každém z modelů teorie T říkáme také formule platí v teorii nebo je splněna v teorii formule 1 + s(0) = s(s(0)) je pravdivá v teorii elementárních čísel Hana Rudová, Logické programování I, 18. března 2007 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/1: s(x):=x není modelem této formule Teorie T jazyka L je množina formulí jazyka L, tzv. axiomů s(X) = 0 je 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: pravdivá v každém z modelů teorie T říkáme také formule platí v teorii nebo je splněna v teorii formule 1 + s(0) = s(s(0)) je pravdivá v teorii elementárních čísel Logicky pravdivá formule F: libovolná interpretace je jejím modelem nebo-li F je pravdivá v každém modelu libovolné teorie formule G G je logicky pravdivá, formule 1 + s(0) = s(s(0)) není logicky pravdivá Hana Rudová, Logické programování I, 18. března 2007 8 Predikátová logika Zkoumání pravdivosti formulí Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F1,. . . , Fn formulí jazyka L, v níž každé Fi je bud' axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel Hana Rudová, Logické programování I, 18. března 2007 9 Predikátová logika Zkoumání pravdivosti formulí Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F1,. . . , Fn formulí jazyka L, v níž každé Fi je bud' axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) 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 Hana Rudová, Logické programování I, 18. března 2007 9 Predikátová logika Zkoumání pravdivosti formulí Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F1,. . . , Fn formulí jazyka L, v níž každé Fi je bud' axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) 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 A, G A odvodit F G Hana Rudová, Logické programování I, 18. března 2007 9 Predikátová logika Zkoumání pravdivosti formulí Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F1,. . . , Fn formulí jazyka L, v níž každé Fi je bud' axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) 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 A, G A odvodit F G F je dokazatelná z formulí A1, , An A1, , An F existuje-li důkaz F z A1, , An Hana Rudová, Logické programování I, 18. března 2007 9 Predikátová logika Zkoumání pravdivosti formulí Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost F1,. . . , Fn formulí jazyka L, v níž každé Fi je bud' axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) 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 A, G A odvodit F G F je dokazatelná z formulí A1, , An A1, , An F existuje-li důkaz F z A1, , An Dokazatelné formule v teorii T nazýváme teorémy teorie T Hana Rudová, Logické programování I, 18. března 2007 9 Predikátová logika Korektnost a úplnost Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) Y ( (0 < Y) ( X (X < Y) ) ) je uzavřená formule ( X (X < Y) ) není uzavřená formule Hana Rudová, Logické programování I, 18. března 2007 10 Predikátová logika Korektnost a úplnost Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) Y ( (0 < Y) ( X (X < Y) ) ) je uzavřená formule ( X (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í P a každou uzavřenou formuli F platí: jestliže P F pak P F (jestliže je něco dokazatelné, pak to platí) Hana Rudová, Logické programování I, 18. března 2007 10 Predikátová logika Korektnost a úplnost Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) Y ( (0 < Y) ( X (X < Y) ) ) je uzavřená formule ( X (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í P a každou uzavřenou formuli F platí: jestliže P F pak P F (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže P F pak P F (jestliže něco platí, pak je to dokazatelné) Hana Rudová, Logické programování I, 18. března 2007 10 Predikátová logika Korektnost a úplnost Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) Y ( (0 < Y) ( X (X < Y) ) ) je uzavřená formule ( X (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í P a každou uzavřenou formuli F platí: jestliže P F pak P F (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže P F pak P F (jestliže něco platí, pak je to dokazatelné) PL1: úplná a korektní dokazatelnost, tj. pro teorii T s množinou axiomů A platí: T F právě když A F Hana Rudová, Logické programování I, 18. března 2007 10 Predikátová logika