Sémantique fonctionnelle pour les QBF non-prénexes
Résumé
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.