Recherche



Accueil Recherche Publications Enseignement Divers


Ma thèse est maintenant disponible ici (version du 13 décembre 2005).

Transparents

        JFPC'06 : "Deux fragments polynomiaux complets pour le problème de la validité des formules booléennes quantifiées" (pdf)

        RFIA'06 : "Fragments propositionnels pour la compilation de connaissances et formules booléennes quantifiées" (pdf)

        Soutenance de thèse : "De la validité des formules booléennes quantifiées : étude de complexité et exploitation de classes traitables au sein d'un prouveur QBF" (pdf)

        AAAI'05 : "Propositional Fragments for Knowledge Compilation and Quantified Boolean Formulae" (pdf)

        SAT'05 : "A Branching Heuristics for Quantified Renamable Horn Formulas" (Slides, Poster)

        RJCIA'05 : "Une heuristique de branchement dirigée vers les formules Horn renommables quantifiées" (pdf)



Les Formules Booléennes Quantifiées (QBF)

  • la page consacrée à mon prouveur qbfl (en français, in english), qui a participé aux évaluations comparatives de prouveurs QBF depuis leur création en 2003.
  • la page consacrée à deux générateurs d'instances QBF polynomiales est disponible ici.

    • J'ai participé à l'AS QBF, l'action spécifique n°83 du département STIC du CNRS au cours de l'année 2002-2003.

    J'étais encadré dans ma recherche par :

    Pierre Marquis

    Sylvie Coste-Marquis

    Daniel Le Berre

    Mes thèmes de recherche sont :

    L'Intelligence Artificielle : le principal domaine de recherche du CRIL.
    La logique propositionnelle : le thème général de mon mémoire de DEA dont le titre est Représentations implicites en logique propositionnelle soutenu en juillet 2002 (sujet, résumé).
    SAT : je suis inscrit parmi les personnes intéressées par le problème SAT sur le site maintenu par Daniel Le Berre SATLive !.
    QBF : une généralisation du problème SAT. C'était également le sujet de ma thèse : les Formules Booléennes Quantifiées. Ces dernières font l'objet de l'AS n°83 du département STIC du CNRS (Algorithmique et problématique expérimentale pour l'évaluation de formules booléennes quantifiées).
    Letombe Florian