De la validité des formules booléennes quantifiées - étude de complexité et exploitation de classes

De la validite des formules booleennes quanti eesDe la validite des formules booleennes quantieesetude de complexite et exploitation de classes traitablesau sein d’un prouveur qbfFlorian LetombeCRIL, CNRS FRE 2499Universite d’Artois, LensEncadrants :Sylvie Coste-MarquisDaniel Le BerrePierre Marquis (Directeur de these)13 decembre 20051/38De la validite des formules booleennes quanti eesIntroductionIntroductionComplexite de qbf pour certains fragments propositionnelsPresentation des fragmentsApercu des preuvesResultats de complexiteUn cas polynomialExploitation de classes traitables au sein d’un prouveur qbfAlgorithmiqueClasses polynomialesQb L’heuristique Resultats experimentauxConclusion et perspectives2/38De la validite des formules booleennes quanti eesIntroductionIntroductionComplexite de qbf pour certains fragments propositionnelsPresentation des fragmentsApercu des preuvesResultats de complexiteUn cas polynomialExploitation de classes traitables au sein d’un prouveur qbfAlgorithmiqueClasses polynomialesQb L’heuristique Resultats experimentauxConclusion et perspectives2/38De la validite des formules booleennes quanti eesIntroductionIntroductionComplexite de qbf pour certains fragments propositionnelsPresentation des fragmentsApercu des preuvesResultats de complexiteUn cas polynomialExploitation de classes traitables au sein d’un prouveur qbfAlgorithmiqueClasses ...