Hodnocení předmětu IBO 1 3 Logické programování I Hana Rudová jaro 2012 Základní informace Přednáška: účast není povinná, nicméně ... Cvičení: účast povinná ■ individuální doplňující příklady za zmeškaná cvičení ■ nelze při vysoké neúčasti na cvičení ■ skupina 01, sudý pátek, první cvičení 24.února ■ skupina 02, lichý pátek, první cvičení 2.března Web předmětu: interaktivní osnova v ISu ■ průsvitky dostupné postupně v průběhu semestru ■ harmonogram výuky, předběžný obsah výuky pro jednotlivé přednášky během semestru ■ elektronicky dostupné materiály ■ informace o zápočtových projektech Hana Rudová, Logické programování I, 18. května 2012 3 Organizace předmětu ■ Průběžná písemná práce: až 30 bodů (základy programování v Prologu) ■ pro každého jediný termín: 22.března ■ alternativní termín pouze v případech závažných důvodů pro neúčast ■ vzor písemky na webu předmětu ■ Závěrečná písemná práce: až 1 50 bodů ■ vzor písemky na webu předmětu ■ opravný termín možnýjako ústní zkouška ■ Zápočtový projekt: celkem až 40 bodů ■ Hodnocení: součet bodů za projekt a za obě písemky ■ známka A za cca 1 75 bodů, známka F za cca 11 0 bodů ■ známka bude zapsána pouze těm, kteří dostanou zápočet za projekt ■ Ukončení předmětu zápočtem: zápočet udělen za zápočtový projekt Hana Rudová, Logickě programování I, 18. května 2012 2 Organizace předmětu Rámcový obsah předmětu Obsah přednášky ■ základy programování v jazyce Prolog ■ teorie logického programováni ■ logické programování s omezujícími podmínkami ■ implementace logického programováni Obsah cvičení ■ zaměřeno na praktické aspekty, u počítačů ■ programování v Prologu ■ logické programování ■ DCC gramatiky ■ logické programování s omezujícími podmínkami Hana Rudová, Logickě programování I, 18. května 2012 4 Organizace předmětu Literatura Bratko, I. Prolog Programming for Artificial Intelligence. Addison-Wesley, 2001. ■ prezenčně v knihovně Clocksin, W. F. - Mellish, Ch. S. Programming in Prolog. Springer, 1 994. Sterling, L. - Shapiro, E. Y. The art of Prolog : advanced programming techniques. MIT Press, 1 987. Nerode, A. - Shore, R. A. Logic for applications. Springer-Verlag, 1 993. ■ prezenčně v knihovně Dechter, R. Constraint Processing. Morgan Kaufmann Publishers, 2003. ■ prezenčně v knihovně - Elektronicky dostupné materiály (viz web předmětu) Hana Rudová, Logické programování I, 18. května 2012 5 Organizace předmětu Zápočtové projekty Týmová práce na projektech, až 3 řešitelé ■ zápočtové projekty dostupné přes web předmětu Podrobné pokyny k zápočtovým projektům na webu předmětu ■ bodování, obsah předběžné zprávy a projektu ■ typ projektu: LP, CLP, DCC ■ CLP a LP: Adriana Strejčkova ■ DCC: Miloš Jakubíček, Vojtěch Kovář Předběžná zpráva ■ podrobné zadání ■ vjakém rozsahu chcete úlohu řešit ■ které vstupní informace bude program používat a co bude výstupem programu ■ scénáře použití programu (tj. ukázky dvojic konkrétních vstupů a výstupů) Průběžná písemná práce ■ Pro každého jediný termín 22. března ■ Alternativní termín pouze v závažných důvodech pro neúčast ■ Celkem až 30 bodů (1 50 závěrečná písemka, 40 projekt) ■ 3 příklady, 40 minut ■ Napsat zadaný predikát, porovnat chování programů ■ Obsah: první čtyři přednášky a první dvě cvičení ■ Oblasti, kterých se budou příklady zejména týkat ■ unifikace ■ seznamy ■ backtracking ■ optimalizace posledního volání ■ řez ■ aritmetika ■ Ukázka průběžné písemné práce na webu Hana Rudová, Logickě programování I, 18. května 2012 6 Organizace předmětu Časový harmonogram k projektům ■ Zveřejnění zadání (většiny) projektů: 27. února ■ Zahájení registrace řešitelů projektu: 7. března, 19:00 ■ Předběžná analýza řešeného problému: 13. dubna ■ Termín pro odevzdání projektů: 18. května ■ Předvádění projektů (po registraci): 21.května - 22.června Hana Rudová, Logickě programování I, 18. května 2012 7 Organizace předmětu Hana Rudová, Logickě programování I, 18. května 2012 8 Organizace předmětu Software: SICStus Prolog Doporučovaná implementace Prologu Dokumentace: http://www.fi.muni.cz/~hanka/sicstus/doc/html Komerční produkt ■ licence pro instalace na domácí počítače studentů Nové IDE pro SICStus Prolog SPIDER ■ dostupné až od verze SICStus 4.1.3 ■ http://www.si cs.se/si cstus/spi der ■ používá Eclipse SDK Podrobné informace dostupné přes web předmětu ■ stažení SICStus Prologu (sw + licenční klíče) ■ pokyny k instalaci (SICStus Prolog, Eclipse, Spider) Hana Rudová, Logické programování I, 18. května 2012 Organizace předmětu Úvod do Prologu SICStus IDE SPIDER & SlCStus Debugging -My Prolog Project'my_module.pio - Eclipse SDK File Edit SCHus Source Navigate Search Project Run Favorites Win do* Help Debug 1» I ■ , ■ | J>. J. 5. jt. ~ = □ M-vanatH t Prolog Top-levd Configuration [SICStus Launch Configuration Typel) N,m. j® Prolog Target ♦ 5u = calk 5iiffK[[a,_7551rc],_181D) = my_predlt_1810) ,3 Prolog Trjp-levd Ptoces Z_ I # acsiutDtbu... fc B " ° P rr.y c-edl (XI : -sufflifíLiít. 'Suffix) is true whin List and iuNn. jk ti-.i. ji id Suŕfu is s suffiscf List, Ills Nfl solutions, Suffi-es are enumerated in descending order of len íiHin.ittinijivill In? improved later!) siiiflliton variables Tcple.d 1 in C: Users penn.aCš-^Ľ i'jntime-EclipseApplicrtion42'My Prolog Project Hana Rudová, Logické programování I, 1 8. května 201 2 no l/B-ft" -n převzato z http://www.si cs.se/si cstus/spide r Organizace předmětu Prolog PROgramming in LOCic ■ část predikátové logiky prvního řádu Deklarativní programování ■ specifikační jazyk, jasná sémantika, nevhodné pro procedurální postupy ■ Co dělat namísto Jak dělat Základní mechanismy ■ unifikace, stromové datové struktury, automatický backtracking Hana Rudová, Logickě programováni I, 18. května 2012 12 Uvod do Prologu Logické programování Historie ■ Rozvoj začíná po roce 1 970 ■ Robert Kowalski - teoretické základy ■ Alain Colmerauer, David Warren (Warren Abstract Machine) - implementace ■ SICStus Prolog vyvíjen od roku 1 985 ■ Logické programování s omezujícími podmínkami - od poloviny 80. let Aplikace ■ rozpoznávání řeči, telekomunikace, biotechnologie, logistika, plánování, data mining, business rules, ... ■ SICStus Prolog—the first 2 5 years, Mats Carlsson, Per Mildner. Theory and Practice of Logic Programming, 12 (1-2): 35-66, 2012. http://arxiv.org/abs/1011.5640. Hana Rudová, Logické programování I, 18. května 2012 13 Úvod do Prologu Program = fakta + pravidla ■ (Prologovský) program je seznam programových klauzulí ■ programové klauzule: fakt, pravidlo ■ Fakt: deklaruje vždy pravdivé věci ■ clovekC novak, 18, student ). ■ Pravidlo: deklaruje věci, jejichž pravdivost závisí na daných podmínkách ■ studujeC X ) :- clovekC X, _Vek, student ). ■ alternativní (obousměrný) význam pravidel pro každé X, pro každé X, X studuje, jestliže X je student, potom Xje student X studuje ■ pracujeC X ) :- clovekC X, _Vek, CoDela ), praceC CoDela ). ■ Predikát: seznam pravidel a faktů se stejným funktorem a aritou ■ značíme: clovek/3, student/l; analogie procedury v procedurálních jazycích, Hana Rudová, Logické programování I, 18. května 2012 14 Úvod do Prologu Komentáře k syntaxi ■ Klauzule ukončeny tečkou ■ Základní příklady argumentů ■ konstanty: (tomas , anna) ... začínají malým písmenem ■ proměnné ■X, Y ... začínají velkým písmenem ■ _, _A, _B ... začínají podtržítkem (nezajímá nás vracená hodnota) ■ Psaní komentářů clovekC novak, 18, student ). % komentář na konci řádku clovekC novotny, 30, učitel ). /* komentář '■'•'/ Hana Rudová, Logické programování 1,18. května 2012 15 Úvod do Prologu Dotaz ■ Dotaz: uživatel se ptá programu, zda jsou věci pravdivé ?- studujeC novak ). % yes splnitelný dotaz ?- studujeC novotny ). % no nesplnitelný dotaz ■ Odpověď na dotaz ■ positivní - dotaz je splnitelný a uspěl ■ negativní - dotaz je nesplnitelný a neuspěl ■ Proměnné jsou během výpočtu instanciovány (= nahrazeny objekty) ■ ?- clovekC novak, 18, Prace ). Prace = student ■ výsledkem dotazuje instanciace proměnných v dotazu ■ dosud nenainstanciovaná proměnná: volná proměnná ■ Prolog umí generovat více odpovědí, pokud existují ?- clovekC novak, Vek, Prace ). % všechna řešení přes ";" Hana Rudová, Logické programování I, 18. května 2012 16 Úvod do Prologu Klauzule = fakt, pravidlo, dotaz Rekurzivní pravidla Klauzule se skládá z hlavy a těla Tělo je seznam cílů oddělených čárkami, čárka = konjunkce Fakt: pouze hlava, prázdné tělo ■ rodic( pavla, robert ). Pravidlo: hlava i tělo ■ upracovany_c"lovekC X ) :- clovekC X, _Vek, Prace ), praceC Prace, tezka ). Dotaz: prázdná hlava, pouze tělo ■ ?- clovekC novak, Vek, Prace ). ?- rodicC pavla, Dite ), rodic( Dite, Vnuk ). predekC X, Z ) :- rodic( X, Z ). predekC X, Z ) predekC X, Z ) rodicC X, Y ), rodicC Y, Z ). rodicC X, Y ), predekC Y, Z ). % CD % (2) % C2") Hana Rudová, Logické programování I, 1 8. května 201 2 Úvod do Prologu Hana Rudová, Logické programování I, 1 8. května 201 2 Úvod do Prologu Příklad: rodokmen rodic( pavla, robert ). rodic( tomas, robert ). rodicC tomas, e "liská ). rodicC robert, anna ). rodicC robert, petr ). rodicC petr, ji rka ). Výpočet odpovědi na dotaz ?- predek(tomas,robert) rodi rodi rodi rodi rodi cC pavla, robert ) . cC tomas, robert ). c C tomas, eli ska ). cC robert, anna ). cC robert, petr ). rodicC petr, jirka ). predekC X, Z ) predekC X, Z ) predekC X, Z ) :- rodicC X, Z ). % CD rodicC X, Z ). rodicC X, Y ), predekC Y, Z ). predek(tomas,robert) dle (1) yes rodic(tomas, robert) % CD % C2') predekC X, Z ) :- rodicC X, Y ), predekC Y, Z ). % C2') Hana Rudová, Logické programování I, 1 8. května 201 2 Úvod do Prologu Hana Rudová, Logické programování I, 1 8. května 201 2 Uvod do Prologu Výpočet odpovědi na dotaz ?- predek(tomas, petr) Odpověď na dotaz s proměnnou predek(tomas, petr) dle (1) dle (2') no rodic( tomas, petr) rodic(tomas, Y) predek( Y, petr) rodicC tomas, robert ). rodicC tomas, eliska ). rodicC robert, petr ). Y=robert dle rodic(tomas, robert) predek( robert, petr) predekC X, Z ) predekC X, Z ) rodicC X, Z ). % (1) rodicC X, Y ), % (2') predekC Y, Z ). dle (1) rodic(robert, petr) yes Hana Rudová, Logické programování I, 18. května 2012 Úvod do Prologu rodicC pavla, robert ). rodicC tomas, robert ). rodicC tomas, eliska ). rodicC robert, anna ). rodicC robert, petr ). rodicC petr, jirka ). predekC X, Z ) :- rodicC X, Z ). predekC X, Z ) :- rodicC X, Y ), predekC Y, Z ). predekCpetr,Potomek) --> ??? predekCrobert,P) --> ??? Hana Rudová, Logické programování I, 18. května 2012 1. P=anna, 2. Potomek=ji rka P=petr, 3. P=jirka Úvod do Prologu Syntaxe a význam Prologovských programu Syntaxe Prologovských programů ■ Typy objektů jsou rozpoznávány podle syntaxe ■ Atom ■ řetězce písmen, čísel, „_" začínající malým písmenem: pavel , pavel_novak, x25 ■ řetězce speciálních znaků: <-->, ====> ■ řetězce v apostrofech: 'Pavel', 'Pavel Novák' ■ Celá a reálná čísla: 0, -1056, 0.35 ■ Proměnná ■ řetězce písmen, čísel, „_" začínající velkým písmenem nebo „_" ■ anonymní proměnná: ma_diteCX) :- rodicC X, _ ). ■ hodnotu anonymní proměnné Prolog na dotaz nevrací: ?- rodicC X, _ ) ■ lexikální rozsah proměnné je pouze jedna klauzule: prvni CX,X,X). prvni CX,X,_). Hana Rudová, Logické programování I, 18. května 2012 24 Syntaxe a význam Prologovských programů Termy ■ Term - datové objekty v Prologu: datum( 1, kveten, 2003 ) ■ funktor: datum ■ argumenty: 1, kveten, 2003 ■ arita - počet argumentů: 3 ■ Všechny strukturované objekty v Prologu jsou stromy ■ trojuhelnikC bod(4,2), bod(6,4), bod(7,l) ) ■ Hlavní funktor termu - funktor v kořenu stromu odpovídající termu ■ trojuhelnikje hlavní funktor v trojuhelnikC bod(4,2), bod(6,4), bod(7,l) ) Hana Rudová, Logické programování I, 18. května 2012 25 Syntaxe a význam Prologovských programů Unifikace Termy S a T jsou unifikovatelné, jestliže 1. SaTjsou konstanty a tyto konstanty jsou identické; 2. S je proměnná a T cokoliv jiného - S je instanciována na T; Tje proměnná a S cokoliv jiného - Tje instanciována na S 3. S a T jsou termy ■ S a T mají stejný funktor a aritu a ■ všechny jejich odpovídající argumenty jsou unifikovatelné ■ výsledná substituce je určena unifikací argumentů Příklady: k = k ... yes, kl = k2 ... no, A = k(2,3) ... yes, k(s,a,1(1)) = A ... yes s(sss(2),B,ss(2)) = s(sss(2),4,ss(2),s(l))... no s(sssCA),4,ss(3)) = s(sss(2),4,ss(A))... no s(sss(A),4,ss(C)) = s(sss(t(B)),4,ss(A))... A=t(B),C=t(B)... yes Hana Rudová, Logické programování I, 18. května 2012 27 Syntaxe a význam Prologovských programů Unifikace ■ Termy jsou unifikovatelné, jestliže ■ jsou identické nebo ■ proměnné v obou termech mohou být instanciovány tak, že termy jsou po substituci identické ■ datumC Dl, Ml, 2003 ) = datum( 1, M2, Y2) operátor = Dl = 1, Ml = M2, Y2 = 2003 ■ Hledáme nejobecnější unifikátor (most generál unifler (MGU) ■ jiné instanciace? ... Dl = 1, Ml = 5 , Y2 = 2003 ... není MCU ■ ?- datumC Dl, Ml, 2003 ) = datum( 1, M2, Y2), Dl = Ml. ■ Test výskytu (occurs check) ?- X=f(X). X = f(f(f(f(f(f(f(f(f(f(...)))))))))) Hana Rudová, Logické programování I, 18. května 2012 26 Syntaxe a význam Prologovských programů Deklarativní a procedurální význam programů ■ p :- q, r. ■ Deklarativní: Co je výstupem programu? ■ p je pravdivé, jestliže q a r jsou pravdivé ■ Z q a r plyne p => význam mají logické relace ■ Procedurální: Jak vypočítáme výstup programu? ■ p vyřešíme tak, že nejprve vyřešíme q a pak r => kromě logických relací je významné i pořadí cílů ■ výstup ■ indikátor yes/no určující, zda byly cíle splněny ■ instanciace proměnných v případě splnění cílů Hana Rudová, Logické programování I, 18. května 2012 28 Syntaxe a význam Prologovských programů Deklarativní význam programu Konjunce "," vs. disjunkce ";" cílů Instance klauzule: proměnné v klauzuli jsou substituovány termem ma_dite(X) :- rodic( X, Y ). ma_dite(petr) :- rodic( petr, Z ). % klauzule % instance klauzule Máme-li program a cíl C, pak deklarativní význam říká: cíl C je splnitelný právě tehdy, když existuje klauzule C v programu taková, že existuje instance I klauzule C taková, že hlava Ije identická s Ca všechny cíle v těle Ijsou pravdivé. cíl ?- ma_dite(petr) . Hana Rudová, Logické programování 1,18. května 2012 Syntaxe a význam Prologovských programů Pořadí klauzulí a cílů Ca) a(l). a(X) :- b(X,Y), a(Y). b(l,l). ?- a(l). (b) a(X) :- b(X,Y), a(Y). a(l). bCl.D. % změněné pořadí klauzulí v programu vzhledem k (a) % nenalezení odpovědi: nekonečný cyklus (c) a(X) :- b(X,Y), c(Y). ?- a(X). b(l,l). c(2). c(l). (d) a(X) :- c(Y), b(X,Y). % změněné pořadí cílů v těle klauzule vzhledem k (c) bCl.D. c(2). c(l) . % náročnější nalezení první odpovědi než u (c) V obou případech stejný deklarativní ale odlišný procedurální význam Hana Rudová, Logické programování I, 18. května 2012 Syntaxe a význam Prologovských programů Konjunce = nutné splnění všech cílů ■ p :- q, r. Disjunkce = stačí splnění libovolného cíle ■ P :- q; r. p :- q. p :- r. ■ priorita středníku je vyšší (viz ekvivalentní zápisy): p :-q, r; s, t, u. P :- Cq, r) ; (s, t, u). P :- q, r. p : - s , t, u . Hana Rudová, Logické programování I, 18. května 2012 Syntaxe a význam Prologovských programů Pořadí klauzulí a cílů II. (1) a(X) :- c(Y), b(X,Y). (2) b(l,l). (3) c(2). (4) c(l). Vyzkoušejte si: (1) a(X) :- b(X,X), c(X). (3) a(X) :- b(Y,X), c(X). (4) b(2,2). (5) b(2,l). (6) c(l). ?- a(X). a(X) dle (1) c(Y), b(X,Y) dle (3j/Ý=2 dle (4)\Y=1 b(X,2) b(X,1) no dle (2) X=1 yes Hana Rudová, Logické programování I, 1 8. května 201 2 Syntaxe a význam Prologovských programů Cvičení: průběh výpočtu a b b c. d. e e g- h. i. b,c,d. e,c,f,g. g,h. h. Jak vypadá průběh výpočtu pro dotaz ?- a. Operátory, aritmetika Hana Rudová, Logické programování I, 18. května 2012 33 Syntaxe a význam Prologovských programu Operátory ■ Infixová notace: 2*a + b*c ■ Prefixová notace: +( *(2,a), *(b,c) ) priorita +: 500, priorita *: 400 ■ prefixovou notaci lze získat predikátem display/l :- display((a:-s(0),b,c)). :-(a, ,(s(0), ,(b,c))) ■ Priorita operátorů: operátor s nejvyšší prioritou je hlavní funktor ■ Uživatelsky definované operátory: zna petr zna alese. zna( petr, alese). ■ Definice operátoru: :- op( 600, xfx, zna ). priorita: i ..i 200 ■ :- opC 1100, xfy, ; ). nestrukturované objekty: 0 :- op( 1000, xfy, , ). p :- q, r; s, t. p :- (q, r) ; (s, t). ; má vyšší prioritu než , ■ :- op( 1200, xfx, :- ). :-má nejvyšší prioritu ■ Definice operátoru není spojena s datovými manipulacemi (kromě spec. případů) Hana Rudová, Logické programování I, 18. května 2012 35 Operátory, aritmetika Typy operátorů ■ Typy operátorů ■ infixové operátory: xfx, xfy, yfx př. xfx = yfx - ■ prefixové operátory: fx, fy př. fx ?- fy- ■ postfixové operátory: xf, yf ■ x a y určují prioritu argumentu ■ x reprezentuje argument, jehož priorita musí být striktně menší než u operátoru ■ y reprezentuje argument, jehož priorita je menší nebo rovna operátoru ■ a-b-c odpovídá (a-b)-c a ne a-(b-c): „-" odpovídá yfx priorita: 500 Hana Rudová, Logické programování I, 18. května 2012 36 Operátory, aritmetika Aritmetika Předdefinované operátory + , -, *, /, '■'•"■'•'mocnina,// celočíselné dělení, mod zbytek po dělení ?- X = 1 + 2. X=l+2 = odpovídá unifikaci ?- X i s 1 + 2. X = 3 „i s" je speciální předdefinovaný operátor, který vynutí evaluaci ■ porovnej: N = (1+1+1+1+1) N i s (1+1+1+1+1) ■ pravá strana musí být vyhodnotitelný výraz (bez proměnné) ■ výraz na pravé straně je nejdříve aritmeticky vyhodnocen a pak unifikován s levou stranou volání?- X i s Y + 1. způsobí chybu Další speciální předdefinované operátory >, <, >=, =<, =:= aritmetická rovnost, =\= aritmetická nerovnost ■ porovnej: 1+2 =:= 2+1 1+2 = 2+1 ■ obě strany musí být vyhodnotitelný výraz: volání ?- 1 < A + 2. způsobí chybu Hana Rudová, Logické programování I, 18. května 2012 37 Operátory, aritmetika Rez, negace Různé typy rovností a porovnání X = Y XaY jsou unifikovatelné X \= Y XaY nejsou unifikovatelné, (také \+ X = Y) X == Y XaY jsou identické porovnej: ?-A == B. ... no ?-A=B, A==B. ... B = A yes X \== Y XaY nejsou identické porovnej: ?- A \== B. ... yes ?- A=B, A \== B. ... A no X i s Y Y je aritmeticky vyhodnoceno a výsledek je přiřazen X X =:= Y X a Y jsou si aritmeticky rovny X =\= Y XaY si aritmeticky nejsou rovny X < Y aritmetická hodnota X je menší než Y (=<, >, >=) X @< Y term X předchází term Y (@=<, @>, @>=) 1. porovnání termů: podle alfabetického n. aritmetického uspořádání 2. porovnání struktur: podle arity, pak hlavního funktoru a pak zleva podle argumentů ?- f( pavel, g(b)) @< f( pavel, h(a)). .. .yes Hana Rudová, Logické programování I, 18. května 2012 Operátory, aritmetika Řez a upnutí f(X,0) f(X,2) f(X,4) X < 3, ! . 3 =< X, X < 6, ! 6 =< X. přidání operátoru řezu , , ! ' ' 6 ?- f(l,Y), Y>2. f(X,0) :- X < 3, !. %(1) f(X,2) :- X < 6, !. %(2) f(X,4). ?- fCl.Y). Smazání řezu v (1) a (2) změní chování programu Upnutí: po splnění podcílů před řezem se už další klauzule neuvažují Hana Rudová, Logické programování I, 18. května 2012 Rez a ořezání Chování operátoru řezu f(X,Y) s(X,Y) s(X,Y) s(X,Y). Y is X + 1. Y is X + 2. f(X,Y) s(X,Y) s(X,Y) s(X,Y), !. Y is X + 1. Y is X + 2. Předpokládejme, že klauzule H :- TI, T2, Tm, ! aktivována voláním cíle C, který je unifikovatelný s H. V momentě, kdy je nalezen řez, existuje řešení cílů TI, ..., Tm ...Tn.je G=h(X,Y) X=1,Y=1 ?- fCl,Z). Z = 2 ? ; Z = 3 ? ; no ?- fCl,Z). Z = 2 ? ; no Ořezání: při provádění řezu se už další možné splnění cílů TI, .. nehledá a všechny ostatní alternativy jsou odstraněny Upnutí: dále už nevyvolávám další klauzule, jejichž hlava je také unifikovatelná s C Tm Y=2 X=2 Ořezání: po splnění podcílů před řezem se už neuvažuje další možné splnění těchto podcílů Smazání řezu změní chování programu ?- h(X,Y). hCl.Y) hC2,Y) tlCY), !. a. tlCD :- b. b tlC2) :- c. / Hana Rudová, Logické programování 1, 18. května 2012 41 Řez, negace Hana Rudová, Logické programování 1, 18 května 2012 42 Řez: návrat na rodiče Řez: příklad ?- a(X). a(x) cCX) :-cCX) :- PCX). v (X). clCX) :-clCX) :- P(X), ! vCX). Cl) a(X) :- h(X,Y). h(xxí (2) a(X) :- d. m/ X 1 tl(Y),!,e(X') upnutí □ PCD- PC2) vC2) (3) h(l,Y) :- tl(Y), !, e(X). Y/l / X (4) h(2,Y) :- a. b,!,e(X') ořezání ?- cC2) ?- clC2) (5) tl(l) :- b. c,!,e(X') d,!,e(X') true ? %PC2) true ? ; %pC2) (6) tl(2) :- c. || true ? %vC2) no no !,e(X') (7) b :- c. | , no (8) b :- d. e(X') (9) d. X/^// NX^/2 (10) e(l) . (11) e(2). ?- cCX) X = 1 ? X = 2 ? X = 2 ? ; %pCD ; %pC2) ; %vC2) ?- clCX) X = 1 ? no ; %pCD ■ Po zpracování klauzule s řezem se vracím až na rodiče této klauzule, tj. a(X) no Hana Rudová, Logické programování 1, 18. května 2012 43 Řez, negace Hana Rudová, Logické programování 1, 18 května 2012 44 hCX,Y) X=l / \ X=2 tlCY) a (vynechej: upnutí) Y=l / \ Y=2 c (vynechej: ořezání) Řez: cvičení 1. Porovnejte chování uvedených programů pro zadané dotazy. a(X,X) :- b(X). a(X,X) :- b(X),!. a(X,X) :- b(X),c. a(X,Y) :- Y i s X+l. a(X,Y) :- Y i s X+l. a(X,Y) :- Y i s X+l. b(X) :- X > 10. b(X) :- X > 10. b(X) :- X > 10. c :- ! . ?- a(X,Y). ?- a(l,Y). ?- a(ll,Y). 2. Napište predikát pro výpočet maxima max( X, Y, Max ) Typy řezu ■ Zlepšení efektivity programu: určíme, které alternativy nemá smysl zkoušet Poznámka: na vstupu pro X očekávám číslo ■ Zelený řez: odstraní pouze neúspěšná odvození ■ f(X,l) :- X >= 0, !. f(X,-l) :- X < 0. bez řezu zkouším pro nezáporná čísla 2. klauzuli ■ Modrý řez: odstraní redundantní řešení ■ f(X,l) :- X >= 0, !. f(0,l). f(X,-l) :- X < 0. bez řezu vrací f(0,l) 2x ■ Červený řez: odstraní úspěšná řešení ■ f(X,l) :- X >= 0, !. f(_X,-l). bez řezu uspěje 2. klauzule pro nezáporná čísla Hana Rudová, Logické programování I, 18. května 2012 45 Řez, negace Negace jako neúspěch ■ Speciální cíl pro nepravdu (neúspěch) fail a pravdu true ■ X a Y nejsou unifikovatelné: different(X, Y) ■ different( X, Y ) :- X = Y, !, fail. different( _X, _Y ). ■ Xje muž: muz(X) muz( X ) :- zena( X ), !, fail. muz( _X ). Hana Rudová, Logické programování I, 18. května 2012 46 Řez, negace Negace jako neúspěch: operátor \+ ■ different(X,Y) :- X = Y, !, fail. muz(X) :- zena(X), !, fail. different(_X,_Y). muz(_X). ■ Unární operátor \+ P ■ jestliže P uspěje, potom \+ P neuspěje \+(P) :- P, !, fail. ■ v opačném případě \+ P uspěje \+(_)■ ■ different( X, Y ) :- \+ X=Y. ■ muz( X ) :- \+ zena( X ). ■ Pozor: takto definovaná negace \+P vyžaduje konečné odvození P Hana Rudová, Logické programování I, 18. května 2012 47 Řez, negace Hana Rudová, Logické programování I, 18. května 2012 Negace a proměnné \+(P) :- P, !, fail. % (I) \+(_). % (ID dobre( citroen ). dobre( bmw ). drahe( bmw ). rozumne( Auto ) :-\+ drahe( Auto ). % (D % (2) % (3) % (4) d ob re (X), rozum n e (X) dle (1), X/citroen rozumne(citroen) dle (4) \+ drahe(citroen) \ dle (II) dle (I) drahe(citroen),!, fail ?- dobre( X ), rozumne( X ). Hana Rudová, Logické programování I, 18. května 2012 □ yes no Bezpečný cíl ?- \+ drahe( citroen ). yes ?- \+ drahe( X ). no ?- rozumne( citroen ). yes ?- rozumne( X ). no \+ Pje bezpečný: proměnné Pjsou v okamžiku volání P instanciovány ■ negaci používáme pouze pro bezpečný cíl P Hana Rudová, Logické programování I, 18. května 2012 Negace a proměnní* \+(P) :- P, !, fail. % (I) \+(_). % (ID dobre( citroen ). % (1) dobre( bmw ). % (2) drahe( bmw ). % (3) rozumne( Auto ) :- % (4) \+ drahe( Auto ). ?- rozumne( X ), dobre( X ). mne(X), dobre(X) dle (4) \+ drahe(X), dobre(X) dle (I) drahe(X),!,fail,dobre(X) dle (3), X/bmw !, fail, dobre(bmw) fail,dobre(bmw) no Hana Rudová, Logické programování I, 1 8. května 201 2 Chování negace ?- \+ drahe( citroen ). ?- \+ drahe( X ). Negace jako neúspěch používá předpoklad uzavřeného světa pravdivé je pouze to, co je dokazatelné ?- \+ drahe( X ). \+ drahe( X ) :- drahe(X),!,fail. yes no \+ drahe( X). z definice \+ plyne: není dokazatelné, že existuje X takové, že drahe( X ) platí tj. pro všechna X platí \+ drahe( X ) ?- drahe( X ). PTÁME SE: existuje X takové, že drahe( X ) platí? ALE: pro cíle s negací neplatí existuje X takové, že \+ drahe( X ) negace jako neúspěch není ekvivalentní negaci v matematické logice Hana Rudová, Logické programování I, 18. května 2012 Predikáty na řízení běhu programu I. řez „!" fai 1: cíl, který vždy neuspěje true: cíl, který vždy uspěje \+ P: negace jako neúspěch \+ P :- P, !, fail; true. once(P): vrátí pouze jedno řešení cíle P once(P) :- P, !. Vyjádření podmínky: P -> Q ; R ■ jestliže platí P tak Q (P -> Q ; R) : - P, ! , Q. ■ v opačném případě R (P -> Q ; R) :- R. ■ príklad: min(X,Y,Z) : - X =< Y -> Z = X ; Z = Y. P -> Q ■ odpovídá: (P -> Q; fail) ■ příklad: zaporne(X) :- number(X) -> X < 0. Hana Rudová, Logické programování I, 18. května 2012 53 Rez, negace Predikáty na řízení běhu programu II. ■ cal 1 (P): zavolá cíl P a uspěje, pokud uspěje P ■ nekonečná posloupnost backtrackovacích voleb: repeat repeat. repeat :- repeat. klasické použití: generuj akci X, proveď ji a otestuj, zda neskončit Hlava :- ... uloz_stav( StaryStav ), repeat, generuje X ), % deterministické: generuj, prováděj, testuj prováděj( X ), testuj C X ), i obnov_stav( StaryStav ), Hana Rudová, Logické programování I, 18. května 2012 54 Řez, negace Reprezentace seznamu ■ Seznam: [a, b, c], prázdný seznam [] ■ Hlava (libovolný objekt), tělo (seznam): .(Hlava, Telo) ■ všechny strukturované objekty stromy - i seznamy ■ funktordva argumenty Seznamy ■ .(a, .cb, .cc, □))) = [a, b, c] ■ notace: [ Hlava | Telo ] = [a | Tel o] Telo je v [a | Tel o] seznam, tedy píšeme [ a, b, c ] = [ a | [ b, c ] ] ■ Lze psát i: [a, b | Tel o] ■ před " |" je libovolný počet prvku seznamu , za " |" je seznam zbývajících prvku ■ [a,b,c] = [a|[b,c]] = [a,b|[c]] = [a,b,c|[]] ■ pozor: [ [a,b] | [c] ] + [ a, b | [c] ] ■ Seznam jako neúplná datová struktura: [a,b,c|T] ■ Seznam = [a,b,c|T], T = [d,e|S], Seznam = [a,b,c,d,e|S] Hana Rudová, Logické programování I, 18. května 2012 56 Seznamy Prvek seznamu ■ member( X, S ) ■ platí: member( b, [a,b,c] ). ■ neplatí: member( b, [[a,b]|[c]] ). ■ Xje prvek seznamu S, když ■ Xje hlava seznamu S nebo memberC X, [ X | _ ] ). %(1) ■ Xje prvek těla seznamu S member( X, [ _ | Telo ] ) :- memberC X, Telo ). %(2) ■ Příklady použití: ■ memberCl,[2,1,3]). ■ member(X,[1,2,3]) . Hana Rudová, Logické programování I, 1 8. května 201 2 57 dle (1). □ yes dle(1). □ yes member(1,[2,1,3,1,4]) | dle (2) member(1,[1,3,1,4]) dle (2) member(1,[3,1,4]) dle (2) member(1 ,[1,4]) dle (2) member(1 ,[4]) | dle (2) member(1,[]) dle (2) no Cvičení: append/2 appendC [], S, S ). % (1) appendC [X|S1], S2, [X|S3] ) :- appendC SI, S2, S3). % (2) :- append([l,2],[3,4],A). I (2) I A=[1|B] I :- append([2],[3,4],B). I (2) I B=[2|C] => A=[1,2|C] I :- append([],[3,4],Q. I CD | C=[3,4] => A=[l,2,3,4], I yes Hana Rudová, Logické programování I, 18. května 2012 Spojení seznamů append( LI, L2, L3 ) Platí: append( [a,b], [c,d], [a,b,c,d] ) Neplatí: appendC [b,a], [c,d], [a,b,c,d] ), appendC [a,[b]], [c,d], [a,b,c,d] ) Definice: ■ pokud je 1. argument prázdný seznam, pak 2. a 3. argument jsou stejné seznamy: appendC □ , S, S ). ■ pokud je 1. argument neprázdný seznam, pak má 3. argument stejnou hlavu jako 1.: appendC [X|S1], S2, [X|S3] ) :- appendC SI, S2, S3). X S1 S2 S3 Hana Rudová, Logické programování I, 1 8. května 201 2 Optimalizace posledního volání Last Call Optimization (LCO) Implementační technika snižující nároky na paměť Mnoho vnořených rekurzivních volání je náročné na paměť Použití LCO umožňuje vnořenou rekurzi s konstantními pamětovými nároky Typický příklad, kdy je možné použití LCO: ■ procedura musí mít pouze jedno rekurzivní volání: v posledním cíli poslední klauzule ■ cíle předcházející tomuto rekurzivnímu volání musí být deterministické ■ p( ...):- ... % žádné rekurzivní volám' v těle klauzule ) % žádné rekurzivní voláni v těle klauzule p(...) :- !, p( ... ). % řez zajišťuje determinismus Tento typ rekurze lze převést na iteraci Hana Rudová, Logické programování I, 18. května 2012 LCO a akumulátor Reformulace rekurzivní procedury, aby umožnila LCO Výpočet délky seznamu length( Seznam, Délka ) lengthC [] , 0 ) . lengthC [ H | T ], Délka ) :- lengthC T, DelkaO ), Délka is 1 + DelkaO. Upravená procedura, tak aby umožnila LCO: % lengthC Seznam, ZapocitanaDelka, CelkovaDelka ): % CelkovaDelka = ZapocitanaDelka + ,,počet prvků v Seznam'' lengthC Seznam, Délka ) :- lengthC Seznam, 0, Délka ). % pomocný predikát lengthC □ , Délka, Délka ). % celková délka = započítaná délka lengthC [ H I T ], A, Délka ) :- A0 is A + 1, lengthC T, A0, Délka ). Přídavný argument se nazývá akumulátor Hana Rudová, Logické programování I, 18. května 2012 61 Seznamy Akumulátor jako seznam Nalezení seznamu, ve kterém jsou prvky v opačném pořadí reverse( Seznam, OpacnySeznam ) ■ reverseC [] , [] ) • reverseC [ H | T ], Opacny ) :-reverseC T, OpacnyT ), appendC OpacnyT, [ H ], Opacny ). ■ naivní reverse s kvadratickou složitosti reverse pomocí akumulátoru s lineární složitostí ■% reverseC Seznam, Akumulátor, Opacny ): % Opacny obdržíme přidáním prvků ze Seznam do Akumulátor v opačném poradi reversef Seznam, OpacnySeznam ) :- reversef Seznam, [], OpacnySeznam). reversef [], S, S ). reversef [ H | T ], A, Opacny ) :- reversef T, [ H | A ], Opacny ). % přidání H do akumulátoru ■ zpětná konstrukce seznamu (srovnej s předchozí dopřednou konstrukcí, např. append) Hana Rudová, Logické programování I, 18. května 2012 63 Seznamy max_list s akumulátorem Výpočet největšího prvku v seznamu max_1i st (Seznam, Max) max_listC[X], X). max_listC[X|T], Max) :-max_li st CT,MaxT), C MaxT >= X, !, Max = MaxT Max = X ). max_listC[H|T],Max) :- max_listCT,H,Max). max_listC[], Max, Max). max_listC[H|T], CastecnyMax, Max) :-C H > CastecnyMax, !, max_listCT, H, Max ) max_listCT, CastecnyMax, Max) ). Hana Rudová, Logické programování I, 18. května 2012 62 Seznamy reverse/2: cvičení reverseC Seznam, OpacnySeznam ) :- % Cl) reverseC Seznam, [], OpacnySeznam). reverseC [], S, S ). % (2) reverseC [ H | T ], A, Opacny ) :- % C3) reverseC T, [ H | A ], Opacny ). ? - reverseC[l,2,3],0). reverseC[l,2,3] ,0) -> CD reverseC[l,2,3], [], 0) - (3) reverseC [2, 3] , [1] , 0) -~ (3) reverseC[3], [2,1], 0) -~ (3) reverseC[] , [3,2,1] , 0) - (2) yes 0=[3,2,1] Hana Rudová, Logické programování I, 18. května 2012 64 Seznamy Neefektivita při spojování seznamů Sjednocení dvou seznamů append( [], S, S ). append( [X|S1], S2, [X|S3] ) :- append( SI, S2, S3 ). ?- append( [2,3], [1], S ). postupné volání cílů: append( [2,3], [1], S ) - append( [3], [1], S') - append( [], [1], S" ) Vždyje nutné projít celý první seznam Hana Rudová, Logické programování I, 18. května 2012 Akumulátor vs. rozdílové seznamy: reverse reverseC [] , [] ) . reverseC [ H | T ], Opacny ) :- reverseC T, OpacnyT ), appendC OpacnyT, [ H ], Opacny ). kvadratická složitost reverseC Seznam, Opacny ) :- reverseOC Seznam, [], Opacny ). reverseOC [] , S, S ) . reverseOC [ H | T ], A, Opacny ) :- reverseOC T, [ H | A ], Opacny ). akumulátor Oineárni) reverseC Seznam, Opacny ) :- reverseOC Seznam, Opacny-[]). reverseOC □ , S-S ) . reverseOC [ H | T ], Opacny-OpacnyKonec ) :- reverseOC T, Opacny-[ H | OpacnyKonec] ). Příklad: operace pro manipulaci s frontou ■ test na prázdnost, přidání na konec, odebrání ze začátku rozdílové seznamy Cl i neárni) Hana Rudová, Logické programování 1,18. května 2012 Rozdílové seznamy Zapamatování konce a připojení na konec: rozdílové seznamy [a,b] = L1-L2 = [a,b|T]-T = [a,b,c|S]-[c|S] = [a,b,c]-[c] Reprezentace prázdného seznamu: L-L A1 i' Z1 A2 Z2 L1 i L2 \ append( Al-Zl, Z1-Z2, A1-Z2 ). LI L2 L3 [2,3] [1] [2,3,1] [2,3|Z1]-Z1 [1|Z2]-Z2 [2,3,1|Z2]-Z2 L3 ■ ?- append( [2,3|Z1]-Z1, [1|Z2]-Z2, S ). S = AI - Z2 = [2,3|Zl] - Z2 = [2,3| [1|Z2] ] - Z2 Zl = [1|Z2] S = [2,3,1|Z2]-Z2 1 Jednotková složitost, oblíbená technika ale není tak flexibilní Hana Rudová, Logické programování I, 18. května 2012 66 Vestavěné predikáty Vestavěné predikáty Predikáty pro řízení běhu programu ■ fail, true,... Různé typy rovností ■ unifikace, aritmetická rovnost, ... Databázové operace ■ změna programu (programové databáze) za jeho běhu Vstup a výstup Všechna řešení programu Testování typu termu ■ proměnná?, konstanta?, struktura?, ... Konstrukce a dekompozice termu ■ argumenty?, funktor?, ... Hana Rudová, Logické programování I, 18. května 2012 Vestavěné predikáty Příklad: databázové operace Caching: odpovědi na dotazyjsou přidány do programové databáze ■ ?- solve( problem, Solution), asserta( solve( problem, Solution) ). ■ :- dynamic solve/2. % nezbytné při použití v SICStus Prologu Příklad: uloz_trojice( Seznámí, Seznam2 ) :-member( XI, Seznámí ), member( X2, Seznam2 ), spocitej_treti( XI, X2, X3 ), assertz( trojice( XI, X2, X3 ) ), f a i 1. uloz_trojice( _, _ ) :- !. Hana Rudová, Logické programování I, 1 8. května 201 2 Vestavěné predikáty Databázové operace Databáze: specifikace množiny relací Prologovský program: programová databáze, kde jsou relace specifikovány explicitně (fakty) i implicitně (pravidly) Vestavěné predikáty pro změnu databáze během provádění programu: assert( Klauzule ) přidání Klauzule do programu asserta( Klauzule ) přidání na začátek assertz( Klauzule ) přidání na konec retract( Klauzule ) smazání klauzule unifikovatelné s Klauzule Pozor: nadměrné použití těchto operací snižuje srozumitelnost programu Hana Rudová, Logické programování I, 1 8. května 201 2 Vestavěné predikáty Vstup a výstup uživatelsky terminal program může číst data ze vstupního proudu (input stream) program může zapisovat data do výstupního proudu (output stream) dva aktivní proudy ■ aktivní vstupní proud ■ aktivní výstupní proud uživatelský terminál - user ■ datový vstup z terminálu user I chápán jako jeden ze vstupních proudů ■ datový výstup na terminál chápán jako jeden z výstupních proudů soubor 1 soubor 2 —ta program —w — user soubor 3 vstupni proudy vystupni proudy Hana Rudová, Logické programováni I, 18. května 2012 Vestavěné predikáty Vstupní a výstupní proudy: vestavěné predikáty ■ změna (otevření) aktivního vstupního/výstupního proudu: see(S)/tell (S) ctěni( Soubor ) :- see( Soubor ), cteni_ze_souboru( Informace ), see( user ). ■ uzavření aktivního vstupního/výstupního proudu: seen/told ■ zjištění aktivního vstupního/výstupního proudu: seeing(S)/te"l"ling(S) ctěni( Soubor ) :- seeing( StarySoubor ), see( Soubor ), cteni_ze_souboru( Informace ), seen, see( StarySoubor ). Hana Rudová, Logické programování I, 18. května 2012 Vestavěné predikáty Příklad čtení ze souboru process_file( Soubor ) :- seeing( StarySoubor ), see( Soubor ), repeat, read( Term ), process_term( Term ), Term == end_of_file, % zjištění aktivního proudu % otevření souboru Soubor % čtení termu Term % manipulace s termem % je konec souboru? seen, see( StarySoubor ). % uzavření souboru % aktivace původního proudu repeat. repeat repeat. % opakování Sekvenční přístup k textovým souborům čtení dalšího termu: read(Term) ■ při čtení jsou termy odděleny tečkou | ?- read(A), read( ahoj(B) ), read( [C,D] ). |: ahoj. ahoj C petre ). [ ahojC 'Petre!' ), jdeme ]. A = ahoj, B = petre, C = ahoj('Petre!'), D = jdeme ■ po dosažení konce souboru je vrácen atom end_of_f i le zápis dalšího termu: write(Term) ?- writeC ahoj ). ?- writeC 'Ahoj Petre!' ). nový řádek na výstup: nl N mezer na výstup: tab(N) čtení/zápis dalšího znaku: getO(Znak) , get(NeprazdnyZnak)/put(Znak) ■ po dosažení konce souboru je vrácena -1 Hana Rudová, Logické programování I, 18. května 2012 Vestavěné predikáty Čtení programu ze souboru Interpretování kódu programu ■ ?- consult(program). ■ ?- consult('program.pl'). ■ ?- consult( [programl, 'program2.pl'] ). Kompilace kódu programu ■ ?- compile( [programl, 'program2.pl']). ■ ?- [program]. ■ ?- [user]. zadávání kódu ze vstupu ukončené CTRL+D ■ další varianty podobně jako u interpretování ■ typické zrychlení: 5 až 10 krát Hana Rudová, Logické programování I, 18. května 2012 75 Vestavěné predikáty Hana Rudová, Logické programování I, 18. května 2012 76 Vestavěné predikáty Všechna řešení ■ Backtracking vrací pouze jedno řešení po druhém ■ Všechna řešení dostupná najednou: bagof/3 , setof/3, findall/3 ■ bagof( X, P, 5 ): vrátí seznam S, všech objektů X takových, že P je splněno vek( petr, 7 ). vek( anna, 5 ). vek( tomas, 5 ) . ?- bagofC Dite, vek( Dite, 5 ), Seznam ). Seznam = [ anna, tomas ] ■ Volné proměnné v cíli P jsou všeobecně kvantifikovány ?- bagofC Dite, vek( Dite, Vek ), Seznam ). Vek = 7, Seznam = [ petr ]; Vek = 5, Seznam = [ anna, tomas ] Hana Rudová, Logické programování I, 18. května 2012 77 Vestavěné predikáty Existenční kvantifikátor „" " ■ Přidání existenčního kvantifikátoru ,," " => hodnota proměnné nemá význam ?- bagofC Dite, Vek"vek( Dite, Vek ), Seznam ). Seznam = [petr,anna,tomas] ■ Anonymní proměnné jsou všeobecně kvantifikovány, i když jejich hodnota není (jako vždy) vracena na výstup ?- bagofC Dite, vek( Dite, _Vek ), Seznam ). Seznam = [petr] ; Seznam = [anna,tomas] ■ Před operátorem „" " může být i seznam ?- bagof( Vek ,[Jméno,Prijmeni]"vekC Jméno, Prijmeni, Vek ), Seznam ). Seznam = [7,5,5] Hana Rudová, Logické programování I, 18. května 2012 79 Vestavěné predikáty Všechna řešení II. ■ Pokud neexistuje řešení bagof(X, P, S) neuspěje ■ bagof: pokud nějaké řešení existuje několikrát, pak S obsahuje duplicity ■ bagof, setof, findall: P je libovolný cíl vekC petr, 7 ). vekC anna, 5 ). vekC tomas, 5 ). ?- bagofC Dite, C vekC Dite, 5 ), Dite \= anna ), Seznam ). Seznam = [ tomas ] ■ bagof, setof, findall: na objekty shromažďované vX nejsou žádná omezení: Xje term ?- bagofC Dite-Vek, vekC Dite, Vek ), Seznam ). Seznam = [petr-7,anna-5,tomas-5] Hana Rudová, Logické programování I, 18. května 2012 78 Vestavěné predikáty Všechna řešení III. ■ setof ( X, P, S ): rozdíly od bagof ■ S je uspořádaný podle @< ■ případné duplicity v S jsou eliminovány ■ findalK X, P, S ): rozdíly od bagof ■ všechny proměnné jsou existenčně kvantifikovány ?- findalK Dite, vek( Dite, Vek ), Seznam ). ^vS jsou shromažďovány všechny možnosti i pro různá řešení => findall uspěje přesně jednou ■ výsledný seznam může být prázdný => pokud neexistuje řešení, uspěje a vrátí S = [] ■ ?- bagofC Dite, vekC Dite, Vek ), Seznam ). Vek = 7, Seznam = [ petr ]; Vek = 5, Seznam = [ anna, tomas ] ?- findallC Dite, vekC Dite, Vek ), Seznam ). Seznam = [petr,anna,tomas] Hana Rudová, Logické programování I, 18. května 2012 80 Vestavěné predikáty Testování typu termu Určení počtu výskytů prvku v seznamu var(X) nonvar(X) atom(X) i nteger(X) float (X) atomi c(X) compound(X) X je volná proměnná X není proměnná X je atom (pavel, 'Pavel Novák', <-->) X je integer X je float X je atom nebo číslo X je struktura count( X, S, N ) :- count( X, S, 0, N ). count( _, [], N, N ). count( X, [X|S], NO, N) :- !, Nl is NO + 1, count( X, S, Nl, N). count( X, [_|S], NO, N) :- count( X, S, NO, N). :-? count( a, [a,b,a,a], N ) N=3 :-? count( a, [a,b,X,Y], N). N=3 count( _, [], N, N ). count( X, [Y|S], NO, N ) :- nonvar(Y), X = Y, !, Nl is NO + 1, count( X, S, Nl, N ). count( X, [_|S], NO, N ) :- count( X, S, NO, N ). Hana Rudová, Logické programování I, 18. května 2012 81 Vestavěné predikáty Konstrukce a dekompozice atomu ■ Atom (opakování) ■ řetězce písmen, čísel, „_" začínající malým písmenem: pavel , pavel_novak, x2, x4_34 ■ řetězce speciálních znaků:+, <->, ===> ■ řetězce v apostrofech: ' Pavel ' , 'Pavel Novák', 'prši', 'ano' ?- 'ano'=A. A = ano ■ Řetězec znaků v uvozovkách ■ př. "ano", "Pavel" ?- A="Pavel". ?- A="ano". A = [80,97,118,101,108] A=[97,110,111] ■ př. použití: konstrukce a dekompozice atomu na znaky, vstup a výstup do souboru ■ Konstrukce atomu ze znaků, rozložení atomu na znaky name( Atom, SeznamASCIIKodu ) nameC ano, [97,110,111] ) nameC ano, "ano" ) Hana Rudová, Logické programování I, 18. května 2012 83 Vestavěné predikáty Hana Rudová, Logické programování I, 18. května 2012 82 Vestavěné predikáty Konstrukce a dekompozice termu ■ Konstrukce a dekompozice termu Term =.. [ Funktor | SeznamArgumentu ] a(9,e) =.. [a,9,e] Cil =.. [ Funktor | SeznamArgumentu ], call( Cil ) atom =. . X => X = [atom] ■ Pokud chci znát pouze funktor nebo některé argumenty, pak je efektivnější: functor( Term, Funktor, Arita ) functorC a(9,e), a, 2 ) functor(atom,atom,0) functor(l,1,0) arg( N, Term, Argument ) argC 2, a(9,e), e) Hana Rudová, Logické programování I, 18. května 2012 84 Vestavěné predikáty Rekurzivní rozklad termu Term je proměnná (var/l), atom nebo číslo (atomic/1) => konec rozkladu Term je seznam ([_!_])=> []... řešen výše jako atomic procházení seznamu a rozklad každého prvku seznamu Term je složený (=../2 , functor/3) => procházení seznamu argumentů a rozklad každého argumentu Příklad: ground/1 uspěje, pokud v termu nejsou proměnné; jinak neuspěje ground(Term) :- atomic(Term), !. ground(Term) :- var(Term), !, fail. groundC[H|T]) :- !, ground(H), ground(T). ground(Term) :- Term =.. [ _Funktor | Argumenty ], groundC Argumenty ). ?- ground(s(2,[a(l,3),b,c],X)). ?- ground(s(2, [a(l,3),b,c])). no yes Hana Rudová, Logické programování I, 18. května 2012 85 Vestavěné predikáty Cvičení: dekompozice termu Napište predikát substitute( Podterm, Term, Podterml, Terml), který nahradí všechny výskyty Podterm v Term termem Podterml a výsledek vrátí v Terml Předpokládejte, že Term a Podterm jsou termy bez proměnných ?- substitute( sin(x), 2*sin(x)*f(sin(x)), t, F ). F=2*t*f(t) Příklad: dekompozice termu I. ■ count_term( Integer, Term, N ) určí počet výskytů celého čísla v termu ■ ?- count_term( 1, a(l,2,b(x,z(a,b,1)),Y), N ). N=2 ■ count_term( X, T, N ) :- count_term( X, T, 0, N). count_term( X, T, NO, N ) :- integer(T), X = T, !, N i s NO + 1. count_term( _, T, N, N ) :- atomic(T), !. count_term( _, T, N, N ) :- var(T), !. count_term( X, T, NO, N ) :- T =.. [ _ | Argumenty ], count_arg( X, Argumenty, NO, N ). count_arg( _, [], N, N ). count_arg( X, [ H | T ], NO, N ) :- count_term( X, H, 0, Nl), N2 i s NO + Nl, count_arg( X, T, N2, N ). ■ ?- count_term( 1, [a,2,[b,c] ,[d,[e,f],Y]] , N ) . count_term( X, T, NO, N ) :- T = [_|_], !, count_arg( X, T, NO, N ). klauzuli přidáme před poslední klauzuli count_term/4 Hana Rudová, Logické programování I, 18. května 2012 86 Vestavěné predikáty Technika a styl programování v Prologu Hana Rudová, Logické programování I, 18. května 2012 87 Vestavěné predikáty Technika a styl programování v Prologu Styl programování v Prologu ■ některá pravidla správného stylu ■ správný vs. špatný styl ■ komentáře Ladění Efektivita Hana Rudová, Logické programování I, 18. května 2012 Technika a styl programování v Prologu Správný styl programování konstrukce setříděného seznamu Seznam3 ze setříděných seznamů Seznámí, Seznam2: merge( Seznámí, Seznam2, Seznam3 ) merge( [2,4,7], [1,3,4,8], [1,2,3,4,4,7,8] ) merge( [], Seznam, Seznam ) merge( Seznam, [], Seznam ). % prevence redundantních řešení merge( [X|Telol], [Y|Telo2], [X|Te"lo3] ) :■ X < Y, !, mergeC Telol, [Y|Telo2], Te"lo3 ). mergeC Seznámí, [Y|Telo2], [Y|Te"lo3] ) :-merge( Seznámí, Te"lo2, Te"lo3 ). Styl programování v Prologu I. ■ Cílem stylistických konvencí je ■ redukce nebezpečí programovacích chyb ■ psaní čitelných a srozumitelných programů, které se dobře ladí a modifikují ■ Některá pravidla správného stylu ■ krátké klauzule ■ krátké procedury; dlouhé procedury pouze s uniformní strukturou (tabulka) ■ klauzule se základními (hraničními) případy psát před rekurzivními klauzulemi ■ vhodnájmena procedur a proměnných ■ nepoužívat seznamy ([. . . ]) nebo závorky ({...}, (...)) pro termy pevné arity ■ vstupní argumenty psát před výstupními ■ struktura programu - jednotné konvence v rámci celého programu, např. ■ mezery, prázdné řádky, odsazení ■ klauzule stejné procedury na jednom místě; prázdné řádky mezi klauzulemi; každý cíl na zvláštním řádku Hana Rudová, Logické programování I, 1 8. května 201 2 90 Technika a styl programování v Prologu Špatný styl programování merge( SI, S2, S3 ) 51 = [], ! , S3 = S2; 52 = [], ! , S3 = SI; 51 = [X|TI], 52 = [Y|T2], ( X < Y, !, Z = X, merge( TI, S2, T3 ); Z = Y, merge( SI, T2, T3) ), 53 = [ Z I T3 ]. % první seznam je prázdný % druhý seznam je prázdný % Z je hlava seznamu S3 Hana Rudová, Logické programování I, 1 8. května 201 2 91 Technika a styl programování v Prologu Hana Rudová, Logické programování I, 1 8. května 201 2 92 Technika a styl programování v Prologu Styl programování v Prologu II. Dokumentace a komentáře Středník „;" může způsobit nesrozumitelnost klauzule ■ nedávat středník na konec řádku, používat závorky ■ v některých případech: rozdělení klauzle se středníkem do více klauzulí Opatrné používání operátoru řezu ■ preferovat použití zeleného řezu (nemění deklarativní sémantiku) ■ červený řez používat v jasně definovaných konstruktech negace: P, !, fail; true \+ P alternativy: Podmínka, !, Cill ; Cil2 Podmínka -> Cill ; Ci 12 Opatrné používání negace „\+" ■ negace jako neúspěch: negace není ekvivalentní negaci v matematické logice Pozor na assert a retract: snižuji transparentnost chování programu Hana Rudová, Logické programování I, 1 8. května 201 2 93 Technika a styl programování v Prologu ■ co program dělá, jak ho používat (jaký cíl spustit a jaké jsou očekávané výsledky), příklad použití ■ které predikáty jsou hlavní (top-level) ■ jak jsou hlavní koncepty (objekty) reprezentovány ■ doba výpočtu a paměťové nároky ■ jaké jsou limitace programu ■ zda jsou použity nějaké speciální rysy závislé na systému ■ jaký je význam predikátů v programu, jaké jsou jejich argumenty, které jsou vstupní a které výstupní (pokud víme) ■ vstupní argumenty „+", výstupní „-" mergeC +Seznaml, +Seznam2, -Seznam3 ) ■ ]menoPredikatu/Anta merge/3 ■ algoritmické a implementační podrobnosti Hana Rudová, Logické programování I, 1 8. května 201 2 94 Technika a styl programování v Prologu Ladění Přepínače na trasování: trace/0, notrace/0 Trasování specifického predikátu: spy/1, nospy/1 ■ spy( merge/3 ) debug/0, nodebug/0: pro trasování pouze predikátů zadaných spy/1 Libovolná část programu může být spuštěna zadáním vhodného dotazu: trasování cíle ■ vstupní informace: jméno predikátu, hodnoty argumentů při volání ■ výstupní informace ■ při úspěchu hodnoty argumentů splňující cíl ■ při neúspěchu indikace chyby ■ nové vyvolání přes stejný cíl je volán při backtrackingu Hana Rudová, Logické programování I, 1 8. května 201 2 95 Technika a styl programování v Prologu Krabičkový (4-branový) model ■ Vizualizace řídícího toku (backtrackingu) na úrovni predikátu ■ Cal 1: volání cíle ■ Exit: úspěšné ukončení volání cíle ■ Fai 1: volání cíle neuspělo ■ Redo: jeden z následujících cílů neuspěl a systém backtrackuje, aby nalezl alternativy k předchozímu řešení | Exit predekC X, Z ) :- rodicC X, Z ). +---------> i predekC X, Z ) :- rodicC X, Y ) , 1 1 predekC Y, Z ). + <--------- | Redo Hana Rudová, Logické programování I, 1 8. května 201 2 96 Technika a styl programování v Prologu Příklad: trasování Efektivita a(X) a(X) a(X) c(l). d(2). nonvar(X). c(X). d(X). Call I ------> + a(X) I a(X) <------+ a(X) Fai 1 I I Exit nonvar(X).| ------> c(X). I d(X). + <------ I Redo I ?- a(X). 1 ? 1 1 Call : a(_463) ? 2 2 Call : nonvarC. _463) ? 2 2 Fai 1 : nonvarC. _463) ? 3 2 Call : c(_463) 7 3 2 Exi t: c Cl) ? 1 1 Exi t: a(l) ? 1 1 Redo: a(l) ? 4 2 Call : d(_463) 7 4 2 Exi t: d(2) ? 1 1 Exi t: a(2) ? X = 2 ? no % trace I ?- Hana Rudová, Logické programování I, 18. května 2012 Technika a styl programování v Prologu Čas výpočtu, paměťové nároky, a také časové nároky na vývoj programu ■ u Prologu můžeme častěji narazit na problémy s časem výpočtu a pamětí ■ Prologovské aplikace redukují čas na vývoj ■ vhodnost pro symbolické, nenumerické výpočty se strukturovanými objekty a relacemi mezi nimi Pro zvýšení efektivity je nutno se zabývat procedurálními aspekty ■ zlepšení efektivity při prohledávání ■ odstranění zbytečného backtrackingu ■ zrušení provádění zbytečných alternativ co nejdříve ■ návrh vhodnějších datových struktur, které umožní efektivnější operace s objekty Hana Rudová, Logické programování I, 18. května 2012 Technika a styl programování v Prologu Zlepšení efektivity: základní techniky ■ Optimalizace posledního volání (LCO) a akumulátory ■ Rozdílové seznamy při spojování seznamů ■ Caching: uložení vypočítaných výsledků do programové databáze - Indexace podle prvního argumentu Predikátová logika l.řádu ■ např. v SICStus Prologu ■ při volání predikátu s prvním nainstaniovaným argumentem se používá hašovací tabulka zpřístupňující pouze odpovídající klauzule ■ zamestnanecC Prijmeni, Krestni]meno, Odděleni, ...) ■ seznamyC [], ...) :- ... . seznamyC [H|T], ...) :- ... . ■ Determinismus: ■ rozhodnout, které klauzule mají uspět vícekrát, ověřit požadovaný determinismus Hana Rudová, Logické programování I, 18. května 2012 Technika a styl programování v Prologu Teorie logického programování Predikátová logika I. řádu (PL1) ■ PROLOG: PROgramming in LOCic, čá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) ■ 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. května 2012 101 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, 18. května 2012 103 Predikátová logika 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: vE:V/t£K,V/:K-l ■ závorky: ),( Hana Rudová, Logické programování I, 18. května 2012 102 Predikátová logika Term, atomická formule, formule ■ Term nad abecedou JA ■ každá proměnná z je term ■ je-li f In z A ati.....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 p/n z a ti.....tn jsou termy, pak p(ti.....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é (-ip), (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, 18. května 2012 104 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ě cei 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/n e JA přiřadí n-ární relaci nad T> Příklad: uspořádání na R ■ jazyk: predikátový symbol menší/2 ■ interpretace: univerzum K; 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, 18. května 2012 105 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" i= 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 i= 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, 18. května 2012 107 Predikátová logika Sémantika formulí ■ Ohodnocení proměnné qp(X): každé proměnném je přiřazen prvek \1\ ■ Hodnota termu
(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 Nepravdivá formule 1 tfv Qj. 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 (q}(zero)) e p a (q?(s(zero))) e p iff (q}(zero)) e p a ((1 + q?(zero)) e p iff <0)epa TU ■ ■ ■ , -.r„} Hi v ■ ■ ■ v Hm v -iTi v ■■■ v -iTu
Hornova klauzule: nejvýše jeden pozitivní literál
' {H.^Ti.....^T„} {H} HTi.....^T„}
■ H v -iTi v ■ ■ ■ v ->Tn H -iTi v ■ ■ ■ v ->Tn
Pravidlo: jeden pozitivní a alespoň jeden negativní literál
■ Prolog: H : - Ti, ■ ■ ■ ,Tn. Matematická logika: H <= Ti a ■ ■ ■ a Tn ■H^T H v-.T H v -.Ti v ■ ■ ■ v -iTn Klauzule: {H,-.Ti.....-iTn]
Fakt: pouze jeden pozitivní literál
■ Prolog: H. Matematická logika: H Klauzule: {H} Cílová klauzule: žádný pozitivní literál
■ Prolog: : - Ti,... Tn. Matematická logika: -iTi v ■ ■ ■ v -iTn Klauzule: {-iTi, ■ ■ ■ ->Tn}
Hana Rudová, Logické programování I, 18. května 2012 131 Rezoluce a logické programování
Hana Rudová, Logické programování I, 18. května 2012 130 Rezoluce a logické programování
Logický program
■ Programová klauzule: právě jeden pozitivní literál (fakt nebo pravidlo)
■ Logický program: konečná množina programových klauzulí
■ Příklad:
■ logický program jako množina klauzulí:
P = {P1.P2.P3}
Pi = {p], Pz = {p,^q}, P3={q]
■ logický program v prologovské notaci: V-
v ■ -a-
q.
■ cílová klauzule: G = {^q, -^p} : -q, p.
Hana Rudová, Logické programování I, 18. května 2012 1 32 Rezoluce a logické programování
Lineární rezoluce pro Hornovy klauzule
Začneme s cílovou klauzulí: Co = G
Boční klauzule vybíráme z programových klauzulí P
G={^q,^p} P={P1,P2,P3}: Pi = {p), P2 = iP,^q}, P3 = iq) :-q,p. p. P--q, q.
{^q,^p} Iq} \/, ,
\/ \/
{-i>} (pJ {^ql lil \/ \/
□ □
Střední klauzule jsou cílové klauzule
Hana Rudová, Logické programování I, 1 8. května 201 2
Rezoluce a logickě programování
Cíle a fakta při lineární rezoluci
■ Věta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespoň jeden cíl a jeden fakt.
■ pokud nepoužiji cíl, mám pouze fakta (1 požit.literál) a pravidla (1 požit.literál a alespoň jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden požit, literál
■ pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 požit.literál a alespoň jeden negat. literál), v rezolventě mi stále zůstávají negativní literály
■ Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli.
■ pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo
■ pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo
■ na dvou faktech rezolvovat nelze
=> dokud nepoužiji cíl pracuji stále s množinou faktů a pravidel
■ pokud použiji v důkazu cílovou klauzulí,
fakta mi ubírají negat.literály, pravidla mi je přidávají,
v rezolventě mám stále samé negativní literály, tj. nelze rezolvovat s dalším cílem
Hana Rudová, Logické programování I, 18. května 2012 135 Rezoluce a logickě programování
Lineární vstupní rezoluce
Vstupní rezoluce na P u {G}
■ (opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny
■ začneme s cílovou klauzulí: Co = G
■ boční klauzule jsou vždy z P (tj. jsou to programové klauzule)
(Opakování:) Lineární rezoluční důkaz C z P je posloupnost dvojic (C0,Bo>, ■ ■ ■ (Cn,Bn) taková, že C = Cn+i a
■ Q a každá i?; jsou prvky P nebo některé Cj,j < í
■ každá Cí+i, í < n je rezolventa C; a Bí
Lineární vstupní (Linear ínput) rezoluce (Ll-rezoluce) C z P u {G}
posloupnost dvojic (Co,Bo), ■ ■ ■ (Cn,Bn) taková, že C = CM+i a
■ Co = G a každá Bi JSOU prvky P lineární rezoluce + vstupní rezoluce
■ každá Cí+i, í < n je rezolventa Q a Bi
Hana Rudová, Logickě programování I, 18. května 2012
Rezoluce a logickě programování
Korektnost a úplnost
1 Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje
rezoluční vyvrácení S pomocí vstupní rezoluce. 1 Korektnost platí stejně jako pro ostatní omezení rezoluce
1 Úplnost Ll-rezoluce pro Hornovy klauzule:
Nechť P je množina programových klauzulí a G cílová klauzule.
Je-li množina P u {G} Hornových klauzulí nesplnitelná,
pak existuje rezoluční vyvrácení P u {G} pomocí Ll-rezoluce.
■ vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná => Ll-rezoluce aplikovaná na (obecnou) formuli nezaručuje,
že nalezeneme důkaz, i když formule platí! 1 Význam Ll-rezoluce pro Hornovy klauzule:
■ P = ÍPl.....Pn], G = {Gl.....Gm\
■ Ll-rezolucí ukážeme nesplnitelnost P\ a ■ ■ ■ a Pn a (-iGi v ■ ■ ■ v -iGm)
■ pokud tedy předpokládáme, že program {Pi.....Pn\ platí,
tak musí být nepravdivá (-iGi v ■ ■ ■ v -iGm), tj. musí platit Gi a ■ ■ ■ a Gm
Hana Rudová, Logickě programování I, 18. května 2012 136 Rezoluce a logickě programování
Uspořádané klauzule (definite clauses)
Klauzule = množina literálů
Uspořádaná klauzule (definite clause) = posloupnost literálů
■ nelze volně měnit pořadí literálů
Rezoluční princip pro uspořádané klauzule:
Í^A0,...,^An} {ď,-.ď0, ...,-.£,„}
{^A0,-lAf-i, -ifioP, ■ ■ ■, ^Bmp, -lAf+i,..., -*A„}cr
■ uspořádaná rezolventa: {-*Ao.....-*Aí-i, -