Predikátová logika l.řádu Teorie logického programování M PROLOG: PROgramming in LOGic, část predikátové logiky 1 .řádu M fakta: rodi c(petr, petri k), VXa(X) ^ klauzule: VXVY rodic(X,Y) => predek(X,Y) Hana Rudová, Logické programování I, 25. března 201 3 2 Teorie logického programování Teorie logického programování 3 PROLOG: PROgramming in LOGic, část predikátové logiky 1 .řádu M fakta: rodi c(petr, petri k), 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, 25. března 201 3 2 Teorie logického programování Teorie logického programování 3 PROLOG: PROgramming in LOGic, část predikátové logiky 1 .řádu M fakta: rodi c(petr, petri k), 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 M Rezoluce ve výrokové logice, v PL1 * dokazovací metoda Rezoluce v logickém programování M Backtracking, řez, negace vs. rezoluce Hana Rudová, Logické programování I, 25. března 201 3 2 Teorie logického programování Predikátová logika I. řádu (PLI) Abeceda J4. jazyka L PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru Hana Rudová, Logické programování I, 25. března 201 3 3 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) M arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) Hana Rudová, Logické programování I, 25. března 201 3 3 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) M arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M 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, 25. března 201 3 3 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) M arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M 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, -i, =>, = Hana Rudová, Logické programování I, 25. března 201 3 3 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda JA jazyka £ PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) M arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M 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, -i, =>, = kvantifikátory V, 3 3 logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) 3 v logice 1. řádu nelze: v R : VA <= R, V/ : R - R Hana Rudová, Logické programování I, 25. března 201 3 3 Predikátová logika Predikátová logika I. řádu (PLI) Abeceda J4. jazyka L PLI se skládá ze symbolů: M proměnné X, Y, ... označují libovolný objekt z daného oboru funkční symboly f, g, ... označují operace (příklad: +, x ) M arita = počet argumentů, n-ární symbol, značíme f/n 3 nulární funkční symboly - konstanty: označují význačné objekty (příklad: 0, 1, ...) M 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, -i, =>, = kvantifikátory V, 3 3 logika I. řádu používá kvantifikaci pouze pro individua (odlišnost od logik vyššího řádu) 3 v logice 1. řádu nelze: v R : VA <= R, V/ : R - R závorky: ),( Hana Rudová, Logické programování I, 25. března 201 3 3 Predikátová logika Jazyky PL1 M 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, 25. března 201 3 4 Predikátová logika Jazyky PLI M 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 M jazyk teorie uspořádání M jazyk s =, binární prediátový symbol < Hana Rudová, Logické programování I, 25. března 201 3 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 3 Jazyky s rovností: obsahují predikátový symbol pro rovnost „=" Příklady jazyk teorie uspořádání M jazyk s =, binární prediátový symbol < M jazyk teorie množin M jazyk s =, binární predikátový symbol e Hana Rudová, Logické programování I, 25. března 201 3 4 Predikátová logika Jazyky PLI 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 M jazyk teorie uspořádání 3 jazyk s =, binární prediátový symbol < jazyk teorie množin M jazyk s =, binární predikátový symbol e M jazyk elementární aritmetiky 3 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, 25. března 2013 4 Predikátová logika Term, atomická formule, formule M Term nad abecedou JA 3 každá proměnná z JA je term M je-li f In z JA 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)) Hana Rudová, Logické programování I, 25. března 201 3 5 Predikátová logika Term, atomická formule, formule M Term nad abecedou SA 3 každá proměnná z JA je term M je-li f In z JA a ři,..., 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)) M Atomická formule (atom) nad abecedou JA M je-li p/n z JA a t\,..., tn jsou termy, pak p(t\,..., tn) je atomická formule f(X) < g(X,0) Hana Rudová, Logické programování I, 25. března 201 3 5 Predikátová logika Term, atomická formule, formule M Term nad abecedou JA 3 každá proměnná z JA je term M je-li f In z JA a t\,..., tn jsou termy, pak f(t\,..., tn) je také term 3 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 M je-li p/n z JA a t\,..., tn jsou termy, pak p(t\,..., tn) je atomická formule f(X) < g(X,0) Formule nad abecedou J4. M každá atomická formule je formule M 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 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, 25. března 201 3 5 Predikátová logika Interpretace Interpretace 1 jazyka L nad abecedou SA je dána M neprázdnou množinou V (také značíme nazývá se univerzum) a M zobrazením, které každé konstantě c g SA přiřadí nějaký prvek T> s* každému funkčnímu symbolu f In g SA přiřadí n-ární operaci nad T> * každému predikátovému symbolu pln g SA přiřadí n-ární relaci nad V Rudová, Logické programování I, 25. března 201 3 6 Predikátová logika Interpretace M Interpretace 1 jazyka L nad abecedou SA je dána neprázdnou množinou T> (také značíme nazývá se univerzum) a 3 zobrazením, které * každé konstantě c g SA přiřadí nějaký prvek T> každému funkčnímu symbolu f In g JA přiřadí n-ární operaci nad T> •9 každému predikátovému symbolu p In g JA přiřadí n-ární relaci nad T> M Příklad: uspořádání na M M jazyk: predikátový symbol mensí/2 3 interpretace: univerzum R; zobrazení: mensí(x,y) := x < y Hana Rudová, Logické programování I, 25. března 201 3 6 Predikátová logika Interpretace M Interpretace 1 jazyka L nad abecedou SA je dána 3 neprázdnou množinou T> (také značíme nazývá se univerzum) a 3 zobrazením, které ± každé konstantě c g JA přiřadí nějaký prvek T> 3 každému funkčnímu symbolu f In g JA přiřadí n-ární operaci nad T> 3 každému predikátovému symbolu pln g JA přiřadí n-ární relaci nad T> M Příklad: uspořádání na M 3 jazyk: predikátový symbol mensí/2 M interpretace: univerzum R; zobrazení: mensi(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 interpretace: &> univerzum N; zobrazení: zero := 0, s(x)\=l+x, plus(x,y) := x + y Hana Rudová, Logické programování I, 25. března 201 3 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 qp(t): každému termu je přiřazen prvek univerza příklad: nechť q>(X) := 0 qp (plus (s (zero), X)) = Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1 Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = q?(s(zero)) + qp(X) = Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1 Hodnota termu qp(t): každému termu je přiřazen prvek univerza M příklad: nechť q?(X) := 0 q?(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(zero)) + 0 = Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza M příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = q?(s(zero)) + q?(X) = (1 + qp(zero)) + 0 = (1 + 0)+ 0 = 1 Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(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 q: formule q označena pravda Nepravdivá formule 1 f^™ q: formule q označena nepravda Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(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 q: formule q označena pravda Nepravdivá formule 1 ^ q: formule q označena nepravda 3 příklad: p II predikátový symbol, tj. p c \1\ p := {(1>, (3>, (5>,...} 1 \= p(zero) a p(s(zero)) Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(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 q: formule q označena pravda Nepravdivá formule 1 ^ q: formule q označena nepravda 3 příklad: p II predikátový symbol, tj. p c \1\ 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, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ 3 Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(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 q: formule q označena pravda Nepravdivá formule 1 ^ q: formule q označena nepravda 3 příklad: p II predikátový symbol, tj. p c \1\ p := {<1>, <3>, <5>,...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (qp(zero)) e p a (qp(s(zero))) e p Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + qp(X) = (1 + qp(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 q: formule q označena pravda Nepravdivá formule 1 ^ q: formule q označena nepravda 3 příklad: pII predikátový symbol, tj. p c \1\ p := {<1>, <3>, <5>,...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (qp(zero)) e p a (qp(s(zero))) e p iff (qp(zero)) e p a <(1 + qp(zero)) e p Hana Rudová, Logické programování I, 25. března 201 3 7 Predikátová logika Sémantika formulí Ohodnocení proměnné qp(X): každé proměnné X je přiřazen prvek \1\ Hodnota termu qp(t): každému termu je přiřazen prvek univerza 3 příklad: nechť qp(X) := 0 qp(plus(s(zero),X)) = qp(s(zero)) + q?(X) = (1 + qp(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 h

, (3>, (5>,...} 1 \= p(zero) a p(s(zero)) iff 1 \= p(zero) a 1 \= p(s(zero)) iff (qp(zero)) e p a (qp(s(zero))) e p iff (qp(zero)) e p a ((1 + qp(zero)) e p iff <0>epaep (1) g p ale (0) é p, tedy formule je nepravdivá v 1 Hana Rudová, Logické programování I, 25. března 201 3 7 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))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Rudová, Logické programování I, 25. března 201 3 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))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Teorie Ť jazyka X je množina formulí jazyka X, tzv. axiomů 3 -i s(X) = Oje jeden z axiomů teorie elementární aritmetiky Hana Rudová, Logické programování I, 25. března 201 3 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))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Teorie Ť jazyka X je množina formulí jazyka X, tzv. axiomů M -i s(X) = Oje jeden z axiomů teorie elementární aritmetiky M Model teorie: libovolná interpretace, která je modelem všech jejích axiomů 3 všechny axiomy teorie musí být v této interpretaci pravdivé Hana Rudová, Logické programování I, 25. března 201 3 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))) 3 interpretace, která se liší přiřazením s/l: s(x):=x není modelem této formule Teorie Ť jazyka X je množina formulí jazyka X, tzv. axiomů M -i s(X) = Oje jeden z axiomů teorie elementární aritmetiky M Model teorie: libovolná interpretace, která je modelem všech jejích axiomů 3 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 Ý 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, 25. března 201 3 8 Predikátová logika Model Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá G je logicky pravdivá, formule 1 + s(0) = s(s(0)) není logicky pravdivá Hana Rudová, Logické programování I, 25. března 201 3 8 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď 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, 25. března 201 3 9 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel M Odvozovací pravidla - příklady M pravidlo modus ponens: z formulí F a F => G lze odvodit G Hana Rudová, Logické programování I, 25. března 201 3 9 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel M Odvozovací pravidla - příklady M pravidlo modus ponens: z formulí F a F => G lze odvodit G M rezoluční princip: z formulí F v A, G v ->A odvodit F v G Hana Rudová, Logické programování I, 25. března 201 3 9 Predikátová logika Zkoumání pravdivosti formulí M Zjištění pravdivosti provádíme důkazem Důkaz: libovolná posloupnost Fi,..., Fn formulí jazyka X, v níž každé Fi je buď axiom teorie jazyka L nebo lze Fi odvodit z předchozích Fj (j < i) použitím určitých odvozovacích pravidel M Odvozovací pravidla - příklady M pravidlo modus ponens: z formulí F a F => G lze odvodit G M rezoluční princip: z formulí F v A, G v ->A odvodit F v G G lze odvodit G M rezoluční princip: z formulí F v A, G v ->A odvodit F v G M F je dokazatelná z formulí Ai, ■ ■ ■ , An Ai, ■ ■ ■ ,An\- F existuje-li důkaz F z Ai, ■ ■ ■ , An 3 Dokazatelné formule v teorii "ľ nazýváme teorémy teorie "ľ Hana Rudová, Logické programování I, 25. března 201 3 9 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) * VY ((0 < Y) A ( EIX (X < Y))) je uzavřená formule 3 ( 3X (X < Y)) není uzavřená formule Hana Rudová, Logické programování I, 25. března 201 3 10 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) 3 VY ((0 < Y) A ( EIX (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 ľNF (jestliže je něco dokazatelné, pak to platí) Hana Rudová, Logické programování I, 25. března 201 3 10 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) 3 VY ((0 < Y) A ( EIX (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 ľNF pak T \- F (jestliže něco platí, pak je to dokazatelné) Hana Rudová, Logické programování I, 25. března 201 3 10 Predikátová logika Korektnost a úplnost M Uzavřená formule: neobsahuje volnou proměnnou (bez kvantifikace) 3 VY ((0 < Y) A ( EIX (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 ľNF (jestliže je něco dokazatelné, pak to platí) Odvozovací pravidla jsou úplná, jestliže jestliže ľNF pak T \- F (jestliže něco platí, pak je to dokazatelné) M PLI: úplná a korektní dokazatelnost, tj. pro teorii Ť s množinou axiomů JA platí: Ť \= F právě když JA \- F Hana Rudová, Logické programování I, 25. března 201 3 10 Predikátová logika