Chapitre 1R´esolution etProgrammation logique1.1 La programmation logique1.1.1 Clause de HornDefinition 1 Une clause de Horn est une disjonction de lit´eraux dont au plusun seul est positif.On les classera en– Fait : p– Buts :¬p ∨...¬p1 n– R`egles : p1∧...∧p ⇒ p (not´ee p:−p ,...,p )n 1 nDefinition 2 Un programme Prolog P est form´e de faits et de r`egles.Une requˆete est une clause qui est un but g.Dans l’´ecriture des programmes PROLOG, les buts sont ´ecrits en omettantla n´egation : on ´ecrit p. au lieu de¬p et p ,...,p au lieu de .¬p ∨...¬p1 n 1 nSi P ∪ {g} est insatisfaisable alors la r´esolution avec une strat´egie bienchoisie permet de d´eduire la clause vide. L’interpr´eteur Prolog utilise la SLDr´esolutionquiestlar´esolutionavecuneregledes´electionparticuli`eredesclauses`ar´esoudre.Cettestrat´egieestcompl`etelorsquelar`egledes´electionest´equitablemais l’impl´ementation usuelle dans les interpr´eteurs Prolog n’est pas compl`ete.1.1.2 Interpr´eteur PrologLa r´esolution est cach´ee dans PROLOG par la notation et la strat´egieutilis´ee, ce qui permet de donner un interpr´eteur PROLOG sans fair r´ef´erence`a la r`egle de r´esolution.1´2 CHAPITRE 1. RESOLUTIONETPROGRAMMATION LOGIQUEL’interpr´eteur prolog est donn´e par la fonction solve. Les buts mentionn´esici sont des atomes, car le calcul par r´esolution est ici implicite. Le calcul desolve(LG,P) correspond a` la r´esolution surC∪{¬g ∨...∨¬g }.1 nsolve(LG,P)/* LG=liste de buts g1,...,gn ...
solve(LG,P) /* LG=liste de buts g1,...,gn (ou vide) Pprogramme=suitedeclauses(faitsoure`gles)C1,...,Cn solve resoud la liste de but LG avec le programme P */ si LG est vide alors retourner Oui sinon g=premier but de LG PP=P Tant que PP n’est pas vide faire C=premiere clause de PP PP=PP \ C si identique(tete(C),g) alors solve(LG {g<corps(C)},P) fsi fait fsi
De´roulementdel’interpre´teurutioesoll’arnestLa’ed´rbrererb –dontlaracineest´etiquet´eeparlebutinitial, –siunnoeudest´etiquet´eparunelistedebutg1, . . . , gn, alors les fils de cenoeudsontlesnoeuds´etiqut´esparB1, . . . , Bm, g2, . . . , gnavecA: −B1, . . . , Bmelquecscesat)(t=md0nalge`renuiafnuuoeA=g1. L’ordre des noeuds est l’ordre des clauses dans le programme. Exemple : Le programme est p. q. r:−p, q. r:−p, q, s. alors pour le but r l’arbre est r / \ echec echecp,q p,q,s / / q echecechec echecq,s echec echec echec | | succes echecs echecechec / \ echec echec echec echec
´ 1.2. SEMANTIQUEPAR POINT FIXE3 1.2S´emantiqueparPointFixe Clauses de Horn et valuation. Un programme prologP´mroedelennftseosopioitprres`egl p1∧. . .∧pn⇒p (n≥1) et defaits: p Unmod`elevesbmelne’lrape´nimreted´steMvdes symboles propositionnels qui valent 1 et on peut identifiervavec cet ensemble. Cela permet de dire qu’un ′ mode`levest plus petit quevsiMv⊆ Mv. ′ Exemple : si P est le programme {p, p⇒q, p∧q⇒r, r⇒q, q∧u⇒rq∧r⇒s} sur PROP={p, q, r, s, t, u, v}ele`domnuali{p,q,r,s}inclus dans tout autre mode`le. Sionconsid`eredesformulesquelconques,lesmode`lesn’ontpasderelation particulie`resentreeux.Parexemple(p∨ ¬qelemod`moem)ca{p},{q},{p, q}. PourlesprogrammesPrologonaunr´esultattr`esfort:l’existenced’unplus petitmode`le.Noterquecere´sultatestfauxpourl’ensembledesclausesdeHorn: ¬p∧ppasdn’a`eleemod. Theore`me1meamgrropoogolprsse`ednuptuoTtmod`elelpsuepit. Soit P un programme Prolog. 1. Sipest un fait du programmePetvnmuedele`doPalorsp∈ Mvpar d´efinition. 2.L’ope´rateurTP:P ROP→P ROPes’otledrre´puetamm´ediatequenceic´snoe associe´`aP)de´finitpar TP(E) ={p| ∃p1∧. . .∧pm⇒p∈P, p1, . . . , pm∈E} Onconside`relasuite: T0=∅ T1=TP(T0) ={p|p fait deP} ... Tn=TP(Tn−1)∪Tn−1 Tn(P)repr´esentecequo’pnuedte´udrieenauplusn−1 utilisations de re`glesdeP. Il existe toujours unn0(nead´dpeprogntduerammP) tel que T(P) =T(P) =. . . n0n0+1 On appelleMµl’ensembleTn0(P) (c’est le point stationnaire de la suite (Tnateup´erel’ofixedpuo)tniorTptrafiein´dT(E) =TP(E)∪E).
´ 4RESOLUTION ET PROGRAMMATION LOGIQUECHAPITRE 1.
3.Toutmod`eleMdePcontientMµrusecm(norrpaertrenrrcu´enqueM contientTn(P) pour toutn. – Vraipourn= 0. –Onsupposequec’estvrai`al’´etapen. SoitMedele`domnutesIlP. mod`eledep1∧. . .∧pm⇒pet sipi∈Tnpouri= 1, . . . , malors ne´cessairementp∈M. DoncTn+1⊆ M. 4.MµnmodestuP.rae`elrtcuocsnesilontile`eodtmelsuotededtiafsP. Soitp1∧. . .∧pm⇒pnuree`lgdeeP. Alors soit un despi6∈ Mµet donc Mµuttourpoitso,elge`raltesdeeolmen`udi= 1, . . . , m,pi∈ Mµet donc par dfinition du point fixep∈ Mµ. Onend´eduit:
Theor`eme2Mµesqugilodeequencesdescons´neesbmelets’lPqui sont des symboles propositionnels.
Ilsuffitdeserappelerquelesconse´quenceslogiquesdePsont les formules vraiesdanstouslesmode`lesdeP.
1.3Correctionetcompl´etudedelaprogramma tion logique Soit P un programme logique. Proposition 1grlororpoundpo´eetni’liSuete´rpriaubut¬palorspest dans lepluspetitmod`eledeP Preuveparinductionsurl’arbreder´esolution. Unestrate´giee´quitablepourlare´solutionestunestrat´egiequiassurequ’un sousbutquipeutˆetrer´esoluleseraparl’interpr´eteur.L’impl´ementationde l’interpre´teurvuecidessusn’estpas´equitable. Proposition 2Soitpequencelunecons´goqieuedPqu´eieegt´rastne.lArouselbati retourne oui au but¬p.