Résolution et programmation logique

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