Constantes : symboles commencant par une minuscule

Variables : symboles commencant par une majuscule

Terme : constante, variable ou symbole de fonction d'arité.

Atome : si p est un symbole de prédicat, p/n est un atome

Littéral : un atome, sa négation

Clause : une clause se note par Atome1<Atome2;Atome3... .

Substitution : on note une substitution par { Variable/Terme; Variable/Terme ... }

Saisie d'un ensemble de clauses.

Saisie d'un but à prouver

Si (But vide)

{

Afficher la substitution courante;

Demander à forcer le Backtrack ?

Si oui, retourner au dernier point de choix;

Sinon Fin = Vrai;

}

Sinon

Examiner si il y a des clauses non explorées pour le predicat But

Si il y en a la prendre;

Si il y en a d'autres les formaliser dans un point de choix;

Si le But s'unifie à la clause par la substitution S

{

Changer la substitution courante par S;

Renommer la substitution S.

Substituer le But et la Clause par S;

Enlever le premier atome du but;

Et rajouter en début du But la suite des atomes de la clause prouvée.

aller en etape1

}

Sinon

aller en étape5

Si il y a encore des clauses non explorées

{

Marqué le choix courant;

Reprendre le but, avec une clause non exploitée;

aller en etape1

}

Sinon

{

Si il y a un pere au point de choix courant

{

Marquer le choix courant;

Prendre le point de choix pere;

Modifier le but, et la clause non exploitée;

retourner en etape6;

}

Sinon

{

Rien n'est prouver;

Fin = Faux ;

}

}

}

etape0 :

Si le nom et l'arité des prédicats sont différents

retour Faux;

etape1 :

Initialisation de la substitution à Vide.

etape2 :

unif = FAUX

pour i de 1 a arite et tant que unif = VRAI

si (symbole de P1 != de symbole de P2)

unif = FAUX;

retour Vrai;

etape3 :

Si p1(i) est une variable et p2(i) est une constante

si on a une substitution p1(i)/k et k!=p2(i)

retour Faux;

sinon

si pas de subsitution pour p1(i)

Ajouter p1(i)/p2(i)

aller en etape2

Si p1(i) est une variable et p2(i) est une variable

si on a deux substitutions pour p1(i) et pour p2(i) différentes

retour Faux;

sinon aller en etape2

Si p1(i) est une fonction d'arité et p2(i) est une fonction d'arite

unifier p1(i) et p2(i) avec la substitution courante

si unification échoue : retour Faux;

sinon aller en etape2

Même tests en échangeant p1(i) par p2(i)

retour Faux;

Soit une substitution S

Pour tous les elements t/k de la substitution

si t et k contiennent une variable identique,

renommer k en k + 1

Soit un prédicat P, et une substitution S

Pour tous les termes t du prédicat

si il existe dans la substitution la substitution t/k

remplacer t par k

MAXSYMB : maximum de symboles gérables

MAXARITE : nombre maximum de terme par prédicat.

VRAI

FAUX

typedef enum symbole { VAR, CON, FON } SYMB;

typedef struct elttab{

char * nom; /* la chaine correspondant au symbole */

SYMB typ; /* le type du symbole */

int indice; /* la valeur lors du renommage */

struct elttab * suiv; /* le symbole suivant dans la table */

} ELTTAB;

Structure

typedef struct clause {

char * nomclause;

int * arite;

ELTTAB sy;

struct clause * cons;

} CLAUSE;

/* Formatage d'une clause a partir d'une chaine */

CLAUSE * SaisieCLA (char * Chaine);

/* Libération d'une clause */

void LibereCLA( CLAUSE ** Clause);

/* Copier une Clause */

CLAUSE * CopieCLA(CLAUSE * Clause);

/* Concatener une clause a une autre */

void ConcatCLA(CLAUSE ** Clause1, CLAUSE * Clause2);

Structure

typedef struct Sub {

ELTTAB * Var; /* Variable */

ELTTAB * Val; /* Valeur */

struct Sub * suiv;

}SUB;

/* Ajouter un item de substitution */

void AjouterSUB(ELTTAB * Var, ELTTAB * Val, SUB ** Sub);

/* Liberer une subsitution */

void LibereSUB(SUB **Sub);

/* Copier une substitution */

SUB * CopieSUB(SUB * Sub);

/* Afficher une substitution */

void AfficherSUB(SUB * Sub);

/* renommage d'une substitution */

void RenommeSUB(SUB * Sub);

Structure

typedef struct PointDeChoix {

struct PointDeChoix * Pere ; /* Pere du point de choix */

CLAUSE * But; /* But a prouver dans le point de choix */

SUB * Sub; /* Substitution lors du point de choix */

struct PointDeChoix * liste ; /* Liste des points de choix fils */

struct PointDeChoix * suiv ; /* Choix frere a explorer */

}PDC;

/* Créer un Point de Choix */

PDC * CreatePDC( CLAUSE * But,

SUB * Sub,

PDC * Pere);

/* Utiliser un Point de Choix */

void UtiliserPDC( PDC * Pdc,

CLAUSE ** But,

SUB ** Sub,

CLAUSE ** Clause);

/* Liberer un Point de Choix */

void LiberePDC( PDC **Pdc);

/* renvoie la premiere clause et complete le point de choix */

CLAUSE * ExamimerClause( PDC * Pdc,

CLAUSE * But,

CLAUSE Liste,

int nbClauses);

/* Substitution d'une Clause */

void Substitue(CLAUSE * Clause, SUB * Sub);

/* Evalue les conditions pour que deux fns d'arite soit unifiable */

SUB * isUnifiable(ELTTAB Sy1, ELTTAB Sy2);

/* Evalue les conditions pour que deux fns d'arite soit unifiable */

int ContradictionSUB(SUB ** Sub1,SUB * Sub2);

{

SUB * SubCourante;

CLAUSE * ClauseCourante;

PDC * PdcCourant;

CLAUSE * ButCourant;

if (But ==NULL)

{

AfficherSUB(SubCourante);

{

char c;

printf(" Bakctrack ?");

scanf("%c", &c);

if (toupper(c)=='0')

goto etape5 ;

}

return VRAI;

}

ClauseCourante = ExamimerClause(PdcCourant, But, Liste, nbClauses);

if (ClauseCourante==NULL)

goto etape5;

if (Unifie(But,Clause,&SubCourante)==VRAI)

{

RenommeSub(SubCourante);

Substitue(ClauseCourante, SubCourante);

Substitue(But, SubCourante);

But = But->cons;

ConcatePRED(Clause->cons,But->cons);

But = Clause->cons;

goto etape1 ;

}

if (PdcCourant->liste!=NULL)

{

PDC * PdcTemp;

PdcCourant = PdcCourant->liste;

Utiliser(PdcCourant, &ButCourant, &SubCourante,&ClauseCourante);

goto etape1;

}

else

if (PdcCourant->suiv!=NULL)

{

PDC * PdcTemp;

PdcTemp = PdcCourant;

PdcCourant = PdcCourant->suiv;

LiberePDC(PdcTemp);

Utiliser(PdcCourant, &ButCourant, &SubCourante,&ClauseCourante);

goto etape1;

}

else

if (PdcCourant->Pere!=NULL)

{

PDC * PdcTemp;

PdcTemp = PdcCourant;

PdcCourant = PdcCourant->pere;

LiberePDC(PdcTemp);

Utiliser(PdcCourant, &ButCourant, &SubCourante,&ClauseCourante);

goto etape1;

}

else

return FAUX ;

}

int Unifie (CLAUSE * C1, CLAUSE * C2, SUB ** Sub);

{

ELTTAB * Sy1= C1->Sy;

ELTTAB * Sy2=C2->Sy;

etape0 :

if (strcmp(C1->nom, C2->nom)!=0)

return FAUX;

if (strcmp(C1->arite, C2->arite)!=0)

return FAUX;

etape1 :

LibereSUB(&(*Sub)); /* Met Sub à NULL */

etape2 :

unif = FAUX;

while (Sy1->suiv!=NULL && unif==VRAI)

{

if (strcmp(Sy1->nom,Sy2->nom)!=0)

{

unif = FAUX;

goto etape3 ;

}

Sy1= Sy1->suiv;

Sy2 = Sy2->suiv;

}

return VRAI;

typedef struct elttab{

char * nom; /* la chaine correspondant au symbole */

SYMB typ; /* le type du symbole */

int indice; /* la valeur lors du renommage */

struct elttab * suiv; /* le symbole suivant dans la table */

etape3 :

if ((Sy1->typ==VAR))

{

AjouterSUB(S1->nom, S2->nom, &Sub);

Substitue(C1, *Sub);

Substitue(C2,*Sub);

goto etape2 ;

}

if ((Sy1->typ==FON) && (Sy2->typ==FON))

{

SUB * SubUnif;

SUB * SubTemp2 = Sub;

SUB * SubTemp3;

SubUnif = isUnifiable(Sy1, Sy2);

if (SubUnif ==NULL)

return FAUX;

if (ContradictionSUB(&SubUnif,Sub)==VRAI)

return FAUX;

AjouterSUB(S1->nom, S2->nom, &Sub);

Substitue(C1, *Sub);

Substitue(C2,*Sub);

goto etape2 ;

}

if ((Sy1->typ==FON) && (Sy2->typ==CON))

return FAUX;

if ((Sy2->typ==VAR))

{

AjouterSUB(S1->nom, S2->nom, &Sub);

Substitue(C1, *Sub);

Substitue(C2,*Sub);

goto etape2 ;

}

if ((Sy2->typ==FON) && (Sy1->typ==FON))

{

SUB * SubUnif;

SUB * SubTemp2 = Sub;

SUB * SubTemp3;

SubUnif = isUnifiable(Sy2, Sy1);

if (SubUnif ==NULL)

return FAUX;

if (ContradictionSUB(&SubUnif,Sub)==VRAI)

return FAUX;

AjouterSUB(S1->nom, S2->nom, &Sub);

Substitue(C1, *Sub);

Substitue(C2,*Sub);

goto etape2 ;

}

return FAUX;

}