Résolution et programmation logique

Description

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 ...

Informations

• Publié par: Odri
• Nombre de lectures: 24
• Langue: Français

Extrait

Chapitre 1

R´esolutionet Programmationlogique

1.1 Laprogrammation logique 1.1.1 Clausede Horn Definition 1xuodtnualetie´arplusUseauclneesrnHodejsidenutdnoitcno un seul est positif. On les classera en – Fait:p – Buts:¬p 1 ∨. . .¬p n –R`egles:p1∧. . .∧p n ⇒p(ee´tonp:−p 1 , . . . , p n ) Definition 2Un programme PrologPoftse´mrafedestitder`egles.e Unerequeˆteestuneclausequiestunbutg.

Dansl’e´crituredesprogrammesPROLOG,lesbutssont´ecritsenomettant lane´gation:on´ecritp.au lieu de¬petp 1 , . . . , p n au lieu de .¬p 1 ∨. . .¬p n SiP ∪ {g}egierat´bienaisftisainstenestvecuionaolut´rsesralaeolaslb choisiepermetdede´duirelaclausevide.L’interpre´teurPrologutiliselaSLD re´solutionquiestlare´solutionavecuneregledese´lectionparticuli`eredesclauses `are´soudre.Cettestrat´egieestcompl`etelorsquelar`egledese´lectionest´equitable maisl’imple´mentationusuelledanslesinterpr´eteursPrologn’estpascompl`ete.

1.1.2Interpr´eteurProlog Lare´solutionestcach´eedansPROLOGparlanotationetlastrate´gie utilis´ee,cequipermetdedonneruninterpr´eteurPROLOGsansfairre´fe´rence a`lar`egleder´esolution.

1

´ 2RESOLUTION ET PROGRAMMATION LOGIQUECHAPITRE 1.

L’interpr´eteurprologestdonn´eparlafonctionsolveiontmetss´ennubseL. icisontdesatomes,carlecalculparr´esolutionesticiimplicite.Lecalculde solve(LG,P)corresponda`lare´solutionsurC ∪ {¬g 1 ∨. . .∨ ¬g n }.

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´eparunelistedebutg 1 , . . . , g n , alors les fils de cenoeudsontlesnoeuds´etiqut´esparB 1 , . . . , B m , g 2 , . . . , g n avecA: −B 1 , . . . , B m elquecscesat)(t=md0nalge`renuiafnuuoeA=g 1 . 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 p 1 ∧. . .∧p n ⇒p (n≥1) et defaits: p Unmod`elevesbmelne’lrape´nimreted´steM v des symboles propositionnels qui valent 1 et on peut identifiervavec cet ensemble. Cela permet de dire qu’un ′ mode`levest plus petit quevsiM v ⊆ M v . ′ 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∈ M v par d´efinition. 2.L’ope´rateurT P :P ROP→P ROPes’otledrre´puetamm´ediatequenceic´snoe associe´`aP)de´finitpar T P (E) ={p| ∃p 1 ∧. . .∧p m ⇒p∈P, p 1 , . . . , p m ∈E} Onconside`relasuite: T 0 =∅ T 1 =T P (T 0 ) ={p|p fait deP} ... T n =T P (T n−1 )∪T n−1 T n (P)repr´esentecequo’pnuedte´udrieenauplusn−1 utilisations de re`glesdeP. Il existe toujours unn 0 (nead´dpeprogntduerammP) tel que T(P) =T(P) =. . . n 0 n 0 +1 On appelleM µ l’ensembleT n 0 (P) (c’est le point stationnaire de la suite (T n ateup´erel’ofixedpuo)tniorTptrafiein´dT(E) =T P (E)∪E).

´ 4RESOLUTION ET PROGRAMMATION LOGIQUECHAPITRE 1.

3.Toutmod`eleMdePcontientM µ rusecm(norrpaertrenrrcu´enqueM contientT n (P) pour toutn. – Vraipourn= 0. –Onsupposequec’estvrai`al’´etapen. SoitMedele`domnutesIlP. mod`eledep 1 ∧. . .∧p m ⇒pet sip i ∈T n pouri= 1, . . . , malors ne´cessairementp∈M. DoncT n+1 ⊆ M. 4.M µ nmodestuP.rae`elrtcuocsnesilontile`eodtmelsuotededtiafsP. Soitp 1 ∧. . .∧p m ⇒pnuree`lgdeeP. Alors soit un desp i 6∈ M µ et donc M µ uttourpoitso,elge`raltesdeeolmen`udi= 1, . . . , m,p i ∈ 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 sousbutquipeutˆetrer´esoluleseraparl’interpr´eteur.L’impl´ementationde l’interpre´teurvuecidessusn’estpas´equitable. Proposition 2Soitpequencelunecons´goqieuedPqu´eieegt´rastne.lArouselbati retourne oui au but¬p.