Outils de la page

Piste:

Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Dernière révision Les deux révisions suivantes
enseignement:logique:projet:2015 [2015/12/14 08:38]
ecoquery [Méthode de résolution par ajout de clauses à une CNF] 		enseignement:logique:projet:2015 [2015/12/15 06:58]
ecoquery [Calcul de résolvantes]
Ligne 432: Ligne 432:
  
   * Une première fonction ''pivot'', étant données deux clauses //cl1// et //cl2//, trouve un littéral //l// de //cl1// tel que //¬l// est présent dans //cl2//. Cette fonction prend les deux clauses en paramètre, ainsi qu'un paramètre ''l_pivot'' qui est un littéral passé par référence. Si //l// existe, la fonction reverra ''true'' et affectera ''l_pivot'' à //l//. Sinon la fonction renvoie simplement ''false''. On codera de préférence cette fonction avec un algorithme linéaire dans la taille des clauses, en s'appuyant sur les remarques suivantes:   * Une première fonction ''pivot'', étant données deux clauses //cl1// et //cl2//, trouve un littéral //l// de //cl1// tel que //¬l// est présent dans //cl2//. Cette fonction prend les deux clauses en paramètre, ainsi qu'un paramètre ''l_pivot'' qui est un littéral passé par référence. Si //l// existe, la fonction reverra ''true'' et affectera ''l_pivot'' à //l//. Sinon la fonction renvoie simplement ''false''. On codera de préférence cette fonction avec un algorithme linéaire dans la taille des clauses, en s'appuyant sur les remarques suivantes:
-    * les représentations des littéraux sont triées dans les clauses((i.e. les itérateurs parcourent entier représentant les littéraux dans l'ordre croissant))+    * les représentations des littéraux sont triées dans les clauses((i.e. les itérateurs parcourent les entiers représentant les littéraux dans l'ordre croissant))
     * si n représente un littéral //l//, alors //¬l// est représenté par n+1 ou n-1.     * si n représente un littéral //l//, alors //¬l// est représenté par n+1 ou n-1.
   * Une seconde fonction ''resolvante'', étant données deux clauses et un littéral dans la première clause, calcule la clause qui est la résolvante des deux premières.   * Une seconde fonction ''resolvante'', étant données deux clauses et un littéral dans la première clause, calcule la clause qui est la résolvante des deux premières.
CC Attribution-Noncommercial-Share Alike 3.0 Unported Sauf mention contraire, le contenu de ce wiki est placé sous les termes de la licence suivante : CC Attribution-Noncommercial-Share Alike 3.0 Unported
enseignement/logique/projet/2015.txt · Dernière modification: 2015/12/15 14:40 de ecoquery Haut de page