Backtracking, unifikace, aritmetika Syntaxe logického programu Term: M univerzální datová struktura (slouží také pro příkazy jazyka) M definovaný rekurzivně M konstanty: číselné, alfanumerické (začínají malým písmenem), ze speciálních znaků (operátory) proměnné: pojmenované (alfanumerické řetězce začínající velkým písmenem), anonymní (začínají podtržítkem) M složený term: funktor, arita, argumenty struktury jsou opět termy Hana Rudová, Logické programování I, 3. března 201 2 2 Backtracking, unifikace, aritmetika Anatomie a sémantika logického programu Program: množina predikátů (v jednom nebo více souborech). M Predikát (procedura) je seznam klauzulí s hlavou stejného jména a arity M Klauzule: věty ukončené tečkou, se skládají z hlavy a těla. Prázdné tělo mají fakta, neprázdné pak pravidla, existují také klauzule bez hlavy - direktivy. Hlavu tvoří literal (složený term), tělo seznam literálů. Literálům v těle nebo v dotazu říkáme cíle. Dotazem v prostředí interpretu se spouští programy či procedury. M př. otec(Otec,Dite) :- rodic(Otec,Dite), muz(Otec). rodic(petr, jana). :- otec(Otec, jana). Sémantika logického programu: procedury = databáze faktů a pravidel = logické formule Hana Rudová, Logické programování I, 3. března 2012 3 Backtracking, unifikace, aritmetika SICStus Debugging - My Prolog Project/my_nnodule.pro - Eclipse SDK File Edit SICStus Source Navigate Search Project Run Favorites Window Help- fil $ SICStus Debu... | • " % Debug sTX^ % D> DD I ^ 3. ^ .(» ^, ^ v ° ^ M= Variables E^X^** Breakpoints] to *í B ^ " n> ^ Prolog Top-level Configuration [SICStus Launch Configuration Type 1] 5» Prolog Target Name Value ♦ Suff [a, _7551, c] = call: suffix[[a,_7551,c],_181u] ❖ X _iaio = rny_predlL1810] [:. Prolog Top-level Process rny_module,pro S3 ^ /* Mode:Prolog \n°- Outline V ir.o d-al e (my_mo dul e, [ my_pre dl /1, my pred3/.3 * rams about exporting undefined predicate ]> ■ usemodule(library(lists), [postfix/5, * yarns about importing undefined predicate suffix/2 4 integrated help (also for user predicatesJ 1[ la Q my_predl/l ■v rny_pred2/2 suffixPList ?SuffbO istrue when List and Suffix are lists and Suffix is a suffix of List. It terminates only if List is proper, and has at most N+l solutions, Suffixes are enumerated in descending order of length, (documentation formatting will be improved Eater!) my_predl(X) :- Suff = [a,Singleton,c], assert(seen xs(X)), £ warns about missing declaration (here dynamic/1) suffix {Suff, X), prelude(Suff, X). $ warns about calling undefined predicate ir.y_pred2 (S, Xs) :- $ varn about non-trivial singleton variables ( foreach(Y,Xs} do write(S, X3) > , ( foreach(Y,Xs}, parair. ( [5] ) do write(S, Xs) > ■ □ SICStus ^^-g] Tasks] BE Problems]^ i. dp ^ m ^ m ~ ° g n ľoptevel 1 in C:/Users/perm,SlCS-AD/runtime-EclipseApplication42/My Prolog Project 2 2 Exit: assert (ray_niodule : seen_xs (_1810)) ? 3 2 Call: suffix([a, 7551,c], 1810) ? I Hana Rudová, Logické programování I, 3. března 201 2 4 Backtracking, unifikace, aritmetika SICStus Prolog: spouštění programu M UNIX: module add sicstus-4.1.3 eclipse % použiváni IDE SPIDER sicstus % použiváni přes při kazový řádek MS Windows: 3 používání IDE SPIDER: z nabídky All Programs -> IDE -> Eclipse 3.7 příkazový řádek: z nabídky All Programs -> IDE -> SICStus Prolog VC9 4.2.0 nastavíme pracovní adresář pomocí File/Working directory, v případě potřeby nastavíme font Settings/Font a uložíme nastavení Settings/Save settings. M Iniciální nastavení SICStus IDE v Eclipse pomocí Help->Cheat Sheets->lnitial set up of paths to installed SICStus Prolog s cestou "C:\Program Files (x86)\SICStus Prolog VC9 4.2.0\bin\sicstus.exe" návod: http://www. si cs. se/sicstus/spider/site/prerequi sites. html#Setti ngLIp Hana Rudová, Logické programování I, 3. března 2012 5 Backtracking, unifikace, aritmetika SICStus Prolog: konzultace M Otevření souboru: File->Open File 3 Přístup k příkazové řádce pro zadávání dotazů: SICStus->Open Toplevel M Načtení programu: tzv. konzultace přímo z Menu: SICStus->Consult Prolog Code (okno s programem aktivní) nebo zadáním na příkazový řádek po uložení souboru (Ctrl+S) ?- consult(rodokmen). pokud uvádíme celé jméno případně cestu, dáváme jej do apostrofů ?- consult('D:\prolog\moje\programy\rodokmen.pl'). M V Eclipse lze nastavit Key bindings, pracovní adresář, ... Hana Rudová, Logické programování I, 3. března 201 2 6 Backtracking, unifikace, aritmetika SICStus Prolog: spouštění a přerušení výpočtu Spouštění programů/procedur/predikátů je zápis dotazů na příkazové řádce (v okně TopLevel, kurzor musí být na konci posledního řádku s | ?-), př. ?- predek(petr,1enka). ?- predek(X,Y). Každý příkaz ukončujeme tečkou. 3 Přerušení a zastavení cyklícího programu: pomocí ikony Restart Prolog p* z okna Toplevel Hana Rudová, Logické programování I, 3. března 201 2 7 Backtracking, unifikace, aritmetika Příklad rodokmen rodič (pet r, filip). rodic(petr, lenka). rodi c(pavel, j an). rodic(adam, petr). rodic(tomas, michal), rodic(michal, radek). rodic(eva, filip). rodic(jana, lenka). rodic(pavla, petr). rodic(pavla, tomas). rodic(lenka, vera). otec(Otec,Dite) :- rodic(Otec,Dite), muz(petr). muz(fi lip). muz(pavel). muz(jan). muz(adam). muz(tomas). muz(mi chal). muz(radek). zena(eva). zena(lenka). zena(pavla). zena(jana). zena(vera). muz(Otec). Hana Rudová, Logické programování I, 3. března 201 2 8 Backtracking, unifikace, aritmetika Backtracking: příklady V pracovním adresáři vytvořte program rodokmen.pl. Načtěte program v interpretu (konzultujte). V interpretu Sicstus Prologu pokládejte dotazy: Je Petr otcem Lenky? M Je Petr otcem Jana? Kdo je otcem Petra? M Jaké děti má Pavla? Ma Petr dceru? M Které dvojice otec-syn známe? Hana Rudová, Logické programování I, 3. března 201 2 9 Backtracking, unifikace, aritmetika Backtracking: řešení příkladů Středníkem si vyžádáme další řešení | ?- otec(petr,1enka). yes | ?- otec(petr,jan). no | ?- otec(Kdo,petr). Kdo = adam ? ; no | ?- rodic(pavla,Dite). Dite = petr ? ; Dite = tomas ? ; no | ?- otec(petr,Dcera),zena(Dcera). Dcera = lenka ? ; no | ?- otec(Otec,Syn),muz(Syn). Syn = filip, Otec = petr ? ; Syn = jan, Otec = pavel ? ; Syn = petr, Otec = adam ? ; Syn = mi chal, Otec = tomas ? ; Syn = radek, Otec = michal ? ; no I ?- Hana Rudová, Logické programování I, 3. března 201 2 10 Backtracking, unifikace, aritmetika Backtracking: příklady II Predikát potomek/2: potomek(Potomek,Předek) :- rodic(Predek,Potomek). potomek(Potomek,Předek) :- rodic(Predek,X), potomek(Potomek,X). Naprogramujte predikáty 3 prababicka(Prababicka,Pravnouce) neviastni_bratr(Nevlastni_bratr,Nevíastni_sourozenec) nápověda: využijte X \== Y (X a Y nejsou identické) Hana Rudová, Logické programování I, 3. března 201 2 Backtracking, unifikace, aritmetika Backtracking: příklady II Predikát potomek/2: potomek(Potomek,Předek) :- rodic(Predek,Potomek). potomek(Potomek,Předek) :- rodic(Predek,X), potomek(Potomek,X). Naprogramujte predikáty prababi cka(Prababi cka,Pravnouce) neviastni_bratr(Neviastni_bratr,Nevíastni_sourozenec) nápověda: využijte X \== Y (X a Y nejsou identické) Řešení: prababicka(Prababicka,Pravnouce):-rodic(Prababicka,Prarodič), zena(Prababicka), rodi c(Prarodi c,Rodi c), rodi c(Rodi c,Pravnouce). Hana Rudová, Logické programování I, 3. března 2012 11 Backtracking, unifikace, aritmetika Backtracking: řešení příkladů II neviastni_bratr(Bratr,Sourozenec):-rodi c(X,Bratr), muz(Bratr), rodic(X,Sourozenec), /* tento test neni nutný, ale zvyšuje efektivitu */ Bratr \== Sourozenec, rodi c(Y,Bratr), Y \== X, rodic(Z,Sourozenec), Z \== X, Z \== Y. /* nevhodné umisteni testu - vypočet "bloudi" v neúspěšných větvich */ nevlastni_bratr2(Bratr,Sourozenec):-rodi c(X,Bratr), rodic(X,Sourozenec), rodi c(Y,Bratr), rodic(Z,Sourozenec), Y \== X, Z \== X, Z \== Y, muz(Bratr). Hana Rudová, Logické programování I, 3. března 201 2 12 Backtracking, unifikace, aritmetika Backtracking: porovnání Nahraďte ve svých programech volání predikátu rodic/2 následujícím predikátem rodic_v/2 rodic_v(X,Y):-rodič(X,Y),print(X),print('? '). Pozorujte rozdíly v délce výpočtu dotazu nevlastni_bratr(filip,X) při změně pořadí testů v definici predikátu nevlastni_bratr/2 M varianta 1: testy co nejdříve správně varianta 2: všechny testy umístěte na konec chybně Co uvidíme po nahrazení predikátu rodic/2 predikátem rodic_v/2 v predikátech nevlastni_bratr/2 a nevlastni_bratr2/2 a spuštění? Hana Rudová, Logické programování I, 3. března 201 2 Backtracking, unifikace, aritmetika I ?- nevlastni_bratr(X,Y). petr? petr? petr? petr? eva? petr? jana? X = fi lip, Y = lenka ? ; petr? pavel? pavel? adam? adam? tomas? tomas? michal? michal? eva? eva? jana? pavla? pavla? pavla? adam? pavla? pavla? pavla? pavla? pavla? pavla? lenka? no I ?- nevlastni_bratr2(X,Y). petr? petr? petr? petr? eva? eva? petr? eva? petr? petr? petr? jana? eva? petr? jana X = fi lip, Y = lenka ? ; petr? petr? petr? petr? eva? jana? petr? eva? petr? petr? petr? jana? jana? petr? jana? pavel? pavel? pavel? pavel? adam? adam? adam? adam? pavla? pavla? adam? pavla? tomas? tomas? tomas? tomas? michal? michal? michal? michal? eva? eva? petr? petr? eva? eva? petr? eva? jana? jana? petr? petr? jana? jana? petr? jana? pavla? pavla? adam? adam? pavla? pavla? adam? pavla? pavla? adam? pavla? pavla? pavla? pavla? pavla? pavla? adam? pavla? pavla? pavla? pavla? lenka? lenka? lenka? lenka? no Hana Rudová, Logické programování I, 3. března 201 2 14 Backtracking, unifikace, aritmetika Backtracking: prohledávání stavového prostoru potomek(Potomek,Předek) :- rodic(Predek,Potomek). potomek(Potomek,Předek) :- rodic(Predek,X), potomek(Potomek,X). M Zkuste předem odhadnout (odvodit) pořadí, v jakém budou nalezeni potomci Pavly? :- potomek(X,pavla). M Jaký vliv má pořadí klauzulí a cílu v predikátu potomek/2 na jeho funkci? rodic(petr, filip). rodic(petr, lenka). rodic(pavel, jan). rodic(adam, petr). rodic(tomas, michal). rodic(michal, radek). rodic(eva, filip). rodic(jana, lenka). rodic(pavla, petr). rodic(pavla, tomas). rodic(lenka, vera). Hana Rudová, Logické programování I, 3. března 2012 15 Backtracking, unifikace, aritmetika Backtracking: řešení III potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). Hana Rudová, Logické programování I, 3. března 201 2 16 Backtracking, unifikace, aritmetika Backtracking: řešení III potomek(Potomek,Předek):-rodic(Predek,Potomek). potomek(Potomek,Předek):-rodic(Predek,X),potomek(Potomek,X). /* varianta la */ potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). potomek(Potomek,Předek):-rodi c(Predek,Potomek). Hana Rudová, Logické programování I, 3. března 2012 16 Backtracking, unifikace, aritmetika Backtracking: řešení III potomek(Potomek,Předek):-rodic(Predek,Potomek). potomek(Potomek,Předek):-rodic(Předek,X),potomek(Potomek,X). /* varianta la */ potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). potomek(Potomek,Předek):-rodi c(Predek,Potomek). /* varianta lb - jine poradi odpovědi, neprimi potomci maji přednost */ Hana Rudová, Logické programování I, 3. března 201 2 16 Backtracking, unifikace, aritmetika Backtracking: řešení III potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). /* varianta la */ potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). potomek(Potomek,Předek):-rodi c(Predek,Potomek). /* varianta lb - jine poradi odpovědi, neprimi potomci maji přednost */ potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-potomek(Potomek,X),rodi c(Predek,X). Hana Rudová, Logické programování I, 3. března 201 2 16 Backtracking, unifikace, aritmetika Backtracking: řešení III potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). /* varianta la */ potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). potomek(Potomek,Předek):-rodi c(Predek,Potomek). /* varianta lb - jine poradi odpovědi, neprimi potomci maji přednost */ potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-potomek(Potomek,X),rodi c(Predek,X). /* varianta 2a - leva rekurze ve druhé klauzuli, na dotaz potomek(X,pavla) výpise odpovědi, pak cykli */ Hana Rudová, Logické programování I, 3. března 201 2 16 Backtracking, unifikace, aritmetika Backtracking: řešení III potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). /* varianta la */ potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). potomek(Potomek,Předek):-rodi c(Predek,Potomek). /* varianta lb - jine poradi odpovědi, neprimi potomci maji přednost */ potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-potomek(Potomek,X),rodi c(Predek,X). /* varianta 2a - leva rekurze ve druhé klauzuli, na dotaz potomek(X,pavla) výpise odpovědi, pak cykli */ potomek(Potomek,Předek):-potomek(Potomek,X),rodi c(Predek,X). potomek(Potomek,Předek):-rodi c(Predek,Potomek). Hana Rudová, Logické programování I, 3. března 201 2 16 Backtracking, unifikace, aritmetika Backtracking: řešení III potomek(Potomek,Předek):-rodi c(Predek,Potomek). potomek(Potomek,Předek):-rodi c(Předek,X),potomek(Potomek,X). /* varianta la */ potomek(Potomek,Předek):-rodic(Predek,X),potomek(Potomek,X). potomek(Potomek,Předek):-rodi c(Predek,Potomek). /* varianta lb - jine poradi odpovedi, neprimi potomci maji přednost */ potomek(Potomek,Předek):-rodic(Predek,Potomek). potomek(Potomek,Předek):-potomek(Potomek,X),rodi c(Predek,X). /* varianta 2a - leva rekurze ve druhé klauzuli, na dotaz potomek(X,pavla) výpise odpovedi, pak cykli */ potomek(Potomek,Předek):-potomek(Potomek,X),rodi c(Predek,X). potomek(Potomek,Předek):-rodic(Predek,Potomek). /* varianta 2b - leva rekurze v prvni klauzuli, na dotaz potomek(X,pavla) hned cykli */ Hana Rudová, Logické programování I, 3. března 2012 16 Backtracking, unifikace, aritmetika Unifikace:příklady Které unifikace jsou korektní, které ne a proč? Co je výsledkem provedených unifikací? 1. a(X)=b(X) 2. X=a(Y) 3. a(X)=a(X,X) 4. X=a(X) 5. jmeno(X,X)=jmeno(Petr,plus) 6. s(l,a(X,q(w)))=s(Y,a(2,Z)) 7. s(l,a(X,q(X)))=s(W,a(Z,Z)) 8. X=Y,P=R,s(l,a(P,q(R)))=s(Z,a(X,Y)) Hana Rudová, Logické programování I, 3. března 201 2 Backtracking, unifikace, aritmetika Unifikace:ph klady Které unifikace jsou korektní, které ne a proč? Co je výsledkem provedených unifikací? 1. a(X)=b(X) 2. X=a(Y) 3. a(X)=a(X,X) 4. X=a(X) 5. jmeno(X,X)=jmeno(Petr,plus) 6. s(l,a(X,q(w)))=s(Y,a(2,Z)) 7. s(l,a(X,q(X)))=s(W,a(Z,Z)) 8. X=Y,P=R,s(l,a(P,q(R)))=s(Z,a(X,Y)) Neuspěje volání 1) a 3), ostatní ano, cyklické struktury vzniknou v případech 4),7) a 8) přestože u posledních dvou mají levá a pravá strana unifikace disjunktní množinyjmen proměnných. Hana Rudová, Logické programování I, 3. března 2012 17 Backtracking, unifikace, aritmetika Mechanismus unifikace Unifikace v průběhu dokazování predikátu odpovídá předávání parametrů při provádění procedury, aleje důležité uvědomit si rozdíly. Celý proces si ukážeme na příkladu predikátu suma/3. suma(0,X,X). /^klauzule A*/ suma(s(X),Y,s(Z)):-suma(X,Y,Z). /^klauzule B*/ pomocí substitučních rovnic při odvozování odpovědi na dotaz ?- suma(s(0),s(0),X0). Hana Rudová, Logické programování I, 3. března 201 2 18 Backtracking, unifikace, aritmetika Mechanismus unifikace II suma(0,X,X). /*A*/ suma(s(X),Y,s(Z)):-suma(X,Y,Z). /*B*/ ?- suma(s(0),s(0),X0). 1. dotaz unifikujeme s hlavou klauzule B, s A nejde unifikovat (1. argument) suma(s(0),s(0),X0) = suma(s(Xl),Yl,s(Zl)) ==> XI = 0, Yl = s(0), s(Zl) = X0 ==> suma(0,s(0),Z1) 2. dotaz (nový podcíl) unifikujeme s hlavou klauzule A, klauzuli B si poznačíme jako další možnost suma(0,s(0),Z1) = suma(0,X2,X2) X2 = s(0), Zl = s(0) ==> X0 = s(s(0)) X0 = s(s(0)) ; 2' dotaz z kroku 1. nejde unifikovat s hlavou klauzule B (1. argument) no Hana Rudová, Logické programování I, 3. března 2012 19 Backtracking, unifikace, aritmetika Vícesměrnost predikátů Logický program lze využít vícesměrně, například jako výpočet kdo je otcem Petra? ?- otec(X,petr) . kolik je 1+1? ?- suma(s(0) ,s(0) ,X) . M test je Jan otcem Petra? ?- otec(jan, petr) . Je 1+1 2??- suma(s(0) ,s(0) ,s((0)) ). M generátor které dvojice otec-dítě známe? ?-otec(X,Y) . Které X a Y dávají v součtu 2? ?- suma(X, Y, s(s(0)) ). ... ale pozor na levou rekurzi, volné proměnné, asymetrii, a jiné záležitosti Následující dotazy ?-suma(X,s(0),Z). ?-suma(s(0),X,Z). nedávají stejné výsledky. Zkuste šije odvodit pomocí substitučních rovnic. Hana Rudová, Logické programování I, 3. března 201 2 20 Backtracking, unifikace, aritmetika Aritmetika Zavádíme z praktických důvodů, ale aritmetické predikáty již nejsou vícesměrné, protože v každém aritmetickém výrazu musí být všechny proměnné instaciovány číselnou konstantou. Důležitý rozdíl ve vestavěných predikátech is/2 vs. =/2 vs. =:=/2 is/2: < konstanta nebo proměnná > is < aritmetický výraz > výraz na pravé straně je nejdříve aritmeticky vyhodnocen a pak unifikován s levou stranou =/2: < libovolný term > = < libovolný term > levá a pravá strana jsou unifikovány "=:="/2 "=\="/2 ">="/2 "=<"/2 < aritmetický výraz > =:= < aritmetický výraz > < aritmetický výraz > =\= < aritmetický výraz > < aritmetický výraz > =< < aritmetický výraz > < aritmetický výraz > >= < aritmetický výraz > levá i pravá strana jsou nejdříve aritmeticky vyhodnoceny a pak porovnány Hana Rudová, Logické programování I, 3. března 2012 21 Backtracking, unifikace, aritmetika Aritmetika: příklady Jak se liší následující dotazy (na co se kdy ptáme)? Které uspějí (kladná odpověď), které neuspějí (záporná odpověď), a které jsou špatně (dojde k chybě)? Za jakých předpokladů by ty neúspěšné případně špatné uspěly? 1. X = Y+ 1 7. 1 + 1 = 1 + 1 13. 1 <= 2 2. X is Y + 1 8. 1 + 1 is 1 + 1 3. X = Y 9. 1 + 2 =:= 2 + 1 4. X==Y 10. X\==Y 5. 1 + 1 = 2 11. X =\= Y 6. 2 = 1 + 1 1 2. 1 + 2 =\= 1 - 2 17. sin(X) =:= sin(2+Y) 14. 1 =< 2 1 5. sin(X) is sin(2) 16. sin(X) = sin(2+Y) Nápověda: '='/2 unifikace, '=='/2 test na identitu, '=:='/2 aritmetická rovnost, '\=='/2 negace testu na identitu, '=\='/2 aritmetická nerovnost Hana Rudová, Logické programování I, 3. března 201 2 22 Backtracking, unifikace, aritmetika Aritmetika: příklady II Jak se liší predikáty sl/3 a s2/3? Co umí sl/3 navíc oproti s2/3 a naopak? sl(0,X,X). sl(s(X),Y,s(Z)):-sl(X,Y,Z). s2(X,Y,Z):- Z i s X + Y. Hana Rudová, Logické programování I, 3. března 201 2 23 Backtracking, unifikace, aritmetika Aritmetika: příklady II Jak se liší predikáty sl/3 a s2/3? Co umí sl/3 navíc oproti s2/3 a naopak? sl(0,X,X). sl(s(X),Y,s(Z)):-sl(X,Y,Z). s2(X,Y,Z):- Z i s X + Y. sl/3 je vícesměrný- umí sčítat, odečítat, generovat součty, ale pracuje jen s nezápornými celými čísly s2/3 umí pouze sčítat, ale také záporná a reálná čísla Hana Rudová, Logické programování I, 3. března 201 2 23 Backtracking, unifikace, aritmetika Závěr Dnešní látku jste pochopili dobře, pokud víte M jaký vliv má pořadí klauzulí a cílu v predikátu potomek/2 na jeho funkci, jak umisťovat testy, aby byl prohledávaný prostor co nejmenší (příklad nevlastni_bratr/2), M k čemu dojde po unifikaci X=a(X), M proč neuspěje dotaz ?- X=2, sin(X) is sin(2). za jakých předpokladů uspějí tyto cíle X=Y, X==Y, X=:=Y, M a umíte odvodit pomocí substitučních rovnic odpovedi na dotazy suma(X,s(0),Z) a suma(s(0),X,Z). Hana Rudová, Logické programování I, 3. března 201 2 24 Backtracking, unifikace, aritmetika