Résolution et programmation logique

Publié par

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 ...
Publié le : samedi 24 septembre 2011
Lecture(s) : 24
Nombre de pages : 4
Voir plus Voir moins
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:¬p1. . .¬pn R`egles:p1. . .pnp(ee´tonp:p1, . . . , pn) Definition 2Un programme PrologPoftse´mrafedestitder`egles.e Unerequeˆteestuneclausequiestunbutg.
Dansle´crituredesprogrammesPROLOG,lesbutssont´ecritsenomettant lane´gation:on´ecritp.au lieu de¬petp1, . . . , pnau lieu de .¬p1. . .¬pn SiP ∪ {g}egierat´bienaisftisainstenestvecuionaolut´rsesralaeolaslb choisiepermetdede´duirelaclausevide.Linterpre´teurPrologutiliselaSLD re´solutionquiestlare´solutionavecuneregledese´lectionparticuli`eredesclauses `are´soudre.Cettestrat´egieestcompl`etelorsquelar`egledese´lectionest´equitable maislimple´mentationusuelledanslesinterpr´eteursProlognestpascompl`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.
Linterpr´eteurprologestdonn´eparlafonctionsolveiontmetss´ennubseL. icisontdesatomes,carlecalculparr´esolutionesticiimplicite.Lecalculde solve(LG,P)corresponda`lare´solutionsurC ∪ {¬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´roulementdelinterpre´teurutioesollarnestLaed´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. . .pnp (n1) et defaits: p Unmod`elevesbmelnelrape´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, pq, pqr, rq, qurqrs} sur PROP={p, q, r, s, t, u, v}ele`domnuali{p,q,r,s}inclus dans tout autre mode`le. Sionconsid`eredesformulesquelconques,lesmode`lesnontpasderelation particulie`resentreeux.Parexemple(p∨ ¬qelemod`moem)ca{p},{q},{p, q}. PourlesprogrammesPrologonaunr´esultattr`esfort:lexistencedunplus petitmode`le.Noterquecere´sultatestfauxpourlensembledesclausesdeHorn: ¬pppasdna`eleemod. Theore`me1meamgrropoogolprsse`ednuptuoTtmod`elelpsuepit. Soit P un programme Prolog. 1. Sipest un fait du programmePetvnmuedele`doPalorsp∈ Mvpar d´enition. 2.Lope´rateurTP:P ROPP ROPesotledrre´puetamm´ediatequenceic´snoe associe´`aP)de´nitpar TP(E) ={p| ∃p1. . .pmpP, p1, . . . , pmE} Onconside`relasuite: T0=T1=TP(T0) ={p|p fait deP} ... Tn=TP(Tn1)Tn1 Tn(P)repr´esentecequopnuedte´udrieenauplusn1 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´ereloxedpuo)tniorTptraein´dT(E) =TP(E)E).
´ 4RESOLUTION ET PROGRAMMATION LOGIQUECHAPITRE 1.
3.Toutmod`eleMdePcontientMµrusecm(norrpaertrenrrcu´enqueM contientTn(P) pour toutn. – Vraipourn= 0. Onsupposequecestvrai`al´etapen. SoitMedele`domnutesIlP. mod`eledep1. . .pmpet sipiTnpouri= 1, . . . , malors ne´cessairementpM. DoncTn+1⊆ M. 4.MµnmodestuP.rae`elrtcuocsnesilontile`eodtmelsuotededtiafsP. Soitp1. . .pmpnuree`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´neesbmeletslPqui sont des symboles propositionnels.
Ilsutdeserappelerquelesconse´quenceslogiquesdePsont les formules vraiesdanstouslesmode`lesdeP.
1.3Correctionetcompl´etudedelaprogrammation logique Soit P un programme logique. Proposition 1grlororpoundpo´eetniliSuete´rpriaubut¬palorspest dans lepluspetitmod`eledeP Preuveparinductionsurlarbreder´esolution. Unestrate´giee´quitablepourlare´solutionestunestrat´egiequiassurequun sousbutquipeutˆetrer´esoluleseraparlinterpr´eteur.Limpl´ementationde linterpre´teurvuecidessusnestpas´equitable. Proposition 2Soitpequencelunecons´goqieuedPqu´eieegt´rastne.lArouselbati retourne oui au but¬p.
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.