Sémantique fonctionnelle pour les QBF non-prénexes

We propose in this article a functional semantics for non-prenex Quantified Boolean Formulae.The proposed formalism is symetrical for validity and non-validity and allows to give different interpretations to the quantifiers.This formalism is also sufficiently flexible to allow the definition of a certificate for the search-based algorithms for non-prenex QBF.Nous proposons dans cet article une sémantique fonctionnelle pour les formules booléennes quantifiées non prénexes.Le formalisme proposé est symétrique vis-à-vis de la validité ou de la non-validté et permet d'associer différentes interprétations aux quantificateurs.Il est aussi suffisemment souple pour permettre de définir la notion de certificat pour les procédures de recherche pour les QBF non prénexes.