| Les deux révisions précédentes
Révision précédente
|
|
enseignement:logique:projet:2015 [2015/12/15 06:58]
ecoquery [Calcul de résolvantes] |
enseignement:logique:projet:2015 [2015/12/15 14:40]
ecoquery [Conversion d'une formule en CNF] |
| On donne l'exemple suivant avec f = //(a ∨ b) ⇒ c//, //m// le dictionnaire tel que //a// est numéroté par 0, //b// par 1, //c// par 2 (la prochaine variable fraîche est donc //next// = 3) et cl ={} un ensemble initialement vide de clauses. On a les appels récursifs suivants : | On donne l'exemple suivant avec f = //(a ∨ b) ⇒ c//, //m// le dictionnaire tel que //a// est numéroté par 0, //b// par 1, //c// par 2 (la prochaine variable fraîche est donc //next// = 3) et cl ={} un ensemble initialement vide de clauses. On a les appels récursifs suivants : |
| * ''tseitin(//(a ∨ b) ⇒ c//, m, cl = {}, 3)'' | * ''tseitin(//(a ∨ b) ⇒ c//, m, cl = {}, 3)'' |
| * ''tseitin(//(a ∨ b)//, cl, 3)'' | * ''tseitin(//(a ∨ b)//, m, cl, 3)'' |
| * ''tseitin(//a//, cl, 3)'' 0 est le lit positif correspondant à //a//, on ajoute rien à cl | * ''tseitin(//a//, m, cl, 3)'' 0 est le lit positif correspondant à //a//, on ajoute rien à cl |
| * ''tseitin(//b//, cl, 3)'' 2 est le lit positif correspondant à //b//, on ajoute rien à cl | * ''tseitin(//b//, m, cl, 3)'' 2 est le lit positif correspondant à //b//, on ajoute rien à cl |
| * on a les 2 branches de //(a ∨ b)// on ajoute donc //(¬p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1) ∧ (p ∨ ¬p2)// à cl pour obtenir ''cl = {{7,0,2},{6,1},{6,3}}'' et 6 est le littéral positif qui code //(a ∨ b)//. Au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 4. | * on a les 2 branches de //(a ∨ b)// on ajoute donc //(¬p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1) ∧ (p ∨ ¬p2)// à cl pour obtenir ''cl = {{7,0,2},{6,1},{6,3}}'' et 6 est le littéral positif qui code //(a ∨ b)//. Au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 4. |
| * ''tseitin(c, cl = {{7,0,2},{6,1},{6,3}}, 4)'' 4 est le lit positif correspondant à //c//, on ajoute rien à cl | * ''tseitin(c, m, cl = {{7,0,2},{6,1},{6,3}}, 4)'' 4 est le lit positif correspondant à //c//, on ajoute rien à cl |
| * on a les 2 branches de //(a ∨ b) ⇒ c// on ajoute donc //(¬p ∨ ¬p1 ∨ p2) ∧ (p ∨ p1) ∧ (p ∨ ¬p2)// à cl pour obtenir ''cl = {{7,0,2},{6,1},{6,3},{9,7,4},{8,6},{8,5}}'' et 8 est le littéral positif qui code //f// (au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 5, mais comme on ne tirera plus de variable fraîche par la suite, cela ne se voit pas) | * on a les 2 branches de //(a ∨ b) ⇒ c// on ajoute donc //(¬p ∨ ¬p1 ∨ p2) ∧ (p ∨ p1) ∧ (p ∨ ¬p2)// à cl pour obtenir ''cl = {{7,0,2},{6,1},{6,3},{9,7,4},{8,6},{8,5}}'' et 8 est le littéral positif qui code //f// (au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 5, mais comme on ne tirera plus de variable fraîche par la suite, cela ne se voit pas) |
| |
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