Résolveur ProLog en caml

Salut.
Apres avoir bataillé pendant un temps certain, je me resigne a venir poster ici. En esperant trouver des gens qui auraient le temps et le talent de me repondre...
Comme dit dans le titre, le probleme est ici de concevoir une simple fonction qui serait un debut de résolveur prolog.
Alors voilà, petite mise en bouche.

let prog1 = [ [a;b;c];[c;e];[e];[b;e] ];;
prog1 est un programme prolog tel que :
a:-b,c
c:-e
e:-
b:-e
Soit en francais : a est vrai si b et c sont vrais
c est vrai si e est vrai
e est vrai sans conditions
b est vrai si e est vrai.
donc b est vrrai, et c et vrai, donc a est vrai..
Jusque là tout va bien.

Maintenant,mon probleme est serai de creer une fonction "demontre" qui etant donné une liste d'elements et un programme , prouve que chaque element de la liste est demontré vrai par le programme...
Et là, je seche un peu...
J'ai commencé, mais cette fonction ne verifie que si les elements de la liste sont présents en singleton dans le programme :(

Code:

---

1 2 3 4 5 6

let rec demontreAux = fun p -> let rec loop = function [] -> true |e::l -> (estmembre [e] p) && demontre p l in loop

---

avec "estmembre" une fonction qui renvoie un boolen si l'element arg1 fait partie de la liste arg2 (p est un programme : une liste de liste)
pour ceux que ca interesse:

Code:

---

1 2 3 4 5 6 7 8 9

let estmembre = fun x l -> ilexiste(fun y->x=y) l     let ilexiste = fun p -> let rec eval = function [] -> false |e::l -> (p e) || (eval l) in eval

---

VOilà... moi j'y arrive plus en tout cas...

salu
si je compran le probléme alors
sans l'utilisation des listes on a modéliser le prob comme le suivant:
***********************************************

Code:

---

1 2 3 4 5 6 7 8

exist(b). exist(c). exist(e). trouve(a,K):-exist(b),exist(c)->K=v. trouve(c,K):-exist(e)->K=v. trouve(e,v). trouve(b,K):-exist(e)->K=v. demontrer(X,v):-exist(X);trouve(X,v).

---

************************************************
explication:
a,b,c,d,e,v : sont des symbole (miniscule en prolog)
K,X,Y: sont des variables (majuscule en prolog)
K: si K=v alors l'arg1 de trouve(arg1,v)est demontrable
**predicat:demontrer(X,v) prend tous les elements demontrable
qui donne une resultat comme:
X=a;-------------car trouve(a,v) sera realser
X=b;-------------car exist(b) dans la base des faits
X=c;------------car exist(c) dans la base des faits
X=d;-------------car trouve(d,v) sera realser
X=e;-------------car exist(e) dans la base des faits
no--------------fin aucun autre reponse
juste ou non:yaisse2:

quote : juste ou non?

->Probablement.
Et merci pour ta réponse...
Cependant, c'est bien une fonction de type 'a list -> 'a list list -> bool qui m'est, non seulement demandé, mais que je désire aussi trouver, rapport au temps que j'y ai deja passé...
Ma connaissance en prolog est limitée, de sorte que je ne saisis pas forcement l'ampleur de ton code...
Sur ce...



-> le caml, c bien, mangez en !

Et au passage, loin de moi l'idée de me faire macher le travail...
Je prefere de loin reflechir ensemble...
Donc, si y'en a que mes explications n'ont pas éclairé, ils peuvent toujours se reporter a :
lien mort
Il y restera pas longtemps...
Bonne journée

Je ne sais pas quelle importance tu as accordes à la complexité de ton programme. Si tu n'en accordes pas (pour l'instant), voici ce que j'essaierais :

- une fonction "clauses" qui renvoie les clauses associées à un élément, telle que :

Code:

---

1 2 3 4 5

clauses a prog1 = [b;c] clauses b prog1 = [e] clauses e prog1 = [] clauses d prog1 = exception

---

- une fonction est_vrai qui renvoie true si l'élément est vrai dans le programme.
Donc dans l'exemple, elle renvoie true pour tous les éléments de a à e sauf d.
Cette fonction renvoie simplement true si les clauses de l'élément sont vide, s'appelle récursivement sur toutes les clauses sinon. si clauses lève une exception, renvoie false.

- ta fonction finale qui vérifie que tous les éléments sont vrais.

Je vois. Pas bête !
pour commencer :
mon programme prolog :

p:-t,m,s
p:-q,r
q
r:-s,t
s
t

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13

type literal = |At of char; let prog1 = [ [At 'p';At 't';At 'm';At 's'];[At 'p';At 'q';At 'r'];[At 'q'];[At 'r';At 's'; At 't'];[At 's'];[At 't']] let rec clause = fun e -> let rec loop = function [] -> [] |((a::b)::l) -> if (e=a) then b::(loop l) else loop l in loop literal -> literal list list -> literal list list

---

Cette fonction renvoie une liste de liste de literal, car, dans l'exemple, p est vrai si t m et s sont vrai, OU si q et r sont vrai...
((t et m et s) ou (q et r)) -> p

La suite dans quelques instants... (ou pas... ^^)

C'est peut-être juste, je ne sais pas comment tu vas continuer par la suite, mais c'est différent de la solution que je t'avais proposé car ta fonction ne fait pas la différence entre un élément qui n'a pas de clause et un élément qui n'est pas dans le programme.

Je voulais juste te prévenir :)

EDIT Désolé, je viens de me rendre compte qu'il FAIT la différence, au temps pour moi :oops: