Thèmes étudiés

Un des problèmes centraux en Informatique Fondamentale est la représentation et la manipulation efficace des expressions booléennes. Une bonne compréhension des diverses représentations des fonctions booléennes et de leurs propriétés fondamentales, en particulier des divers types de complexité qui peuvent être définis sur ces représentations et des distributions de probabilité qui leur sont associées, a un intéret évident dans nombre de domaines: conception de circuits, satisfiabilité de fonctions booléennes, avec les phénomènes de seuil sous-jacents, résolution de contraintes, etc. Par exemple, Lefmann et Savicky ont établi un lien entre un certain type de  représentation arborescente d'une fonction booléenne (les arbres Et/Ou) et sa complexité: la connaissance de la probabilité d'apparition d'une fonction f  permet de donner des bornes sur la complexité de f. Les techniques énumératives, analytiques et probabilistes développées pour l'étude des structures arborescentes trouvent ici un nouveau champ d'application.

Le travail développé dans l'équipe concerne d'abord la définition et l'évaluation des probabilités en arbre sur les fonctions booléennes, ainsi que l'étude des liens entre la probabilité d'une fonction booléenne et sa complexité en arbre (plus petite taille d'un arbre représentant la fonction).

Un deuxième axe s'intéresse à la comparaison de la puissance d'expression de différents systèmes du calcul propositionnel; cette puissance d'expression est en général liée au comportement de diverses classes de tautologies dans le système en question.

Naturellement, des questions similaires (dénombrement des formules de taille donnée, lois de probabilité pouvant être définies sur l'ensemble des formules constructibles dans un systeme donné) se posent lorsqu'on sort du calcul des propositions. Nous avons choisi d'étudier les lambda-termes, qui peuvent être vus comme des formules logiques construites sur un seul quantificateur -- et qui sont aussi, vus sous un autre angle, des graphes dirigés acycliques. Alors que les formules du calcul des propositions restaient représentables par des arbres, pour lesquels les outils de la combinatoire analytique sont particulierement appropriés, l'étude des lambda-termes fait apparaître des comportements nouveaux, et requiert des techniques elles aussi nouvelles.

Enfin, le dernier thème développé concerne les problemes de satisfiabilité. Chercher la probabilité qu'une formule booléenne ne soit pas satisfiable revient à chercher la probabilité qu'elle calcule Faux: ce probleme peut être approché par les mêmes techniques que celles utilisées pour étudier les distributions en arbres des fonctions booléennes -- si ce n'est que la forme tres particulière des formules concernées impose, là aussi, l'emploi de nouvelles techniques.

Our website is protected by DMC Firewall!