dernière modification : février 2005
Les travaux de l'équipe se déclinent selon deux thèmes :
Représentation logique des connaissances :
La logique fournit un formalisme très adapté au traitement de divers problèmes de représentation de connaissances. Elle offre un système formel bien défini avec un mécanisme de déduction et une sémantique bien étudiés. Les recherches sur les procédures de preuve et les algorithmes de résolution de problèmes ont fait beaucoup de progrès et plusieurs systèmes basés sur des formalismes logiques sont opérationnels. Toutefois, en représentation des connaissances, la logique classique s'est montrée insuffisante. Elle ne permet pas toujours de prendre en compte le raisonnement révisable et de sens commun, ni le raisonnement spatial et temporel. Notre équipe contribue aux recherches sur les raisonnements non-standards avec des travaux sur les logiques non-monotones, les théories argumentatives et la révision des croyances. Nous nous intéressons plus particulièrement aux X-logiques, formalisme proposés par Siegel, qui généralise la logique classique tout en proposant un cadre unificateur pour les formalismes non-monotones connus les plus importants (modèles préférentiels, circonscription, défauts). Nous nous concentrons actuellement sur deux aspects :
- D'une part la sémantique des X-logiques ; nous attendons de la constitution d'une sémantique qu'elle nous permette de dégager de façon claire des propriétés sur la calculabilité des X-logiques, en particulier par la définition d'un calcul des séquents. Un premier pas a été fait dans ce sens avec l'élargissement des notions classiques de tautologie et de contradiction à celles de X-tautologies et de X-contradictions.
- D'autre part l'application des X-logiques aux théories argumentatives ; nous montrons que l'inférence non-monotone associée aux X-logiques permet de reconsidérer la question peu étudiée de la génération d'arguments pertinents, mais aussi celle de la confrontation entre arguments, au centre de nombreux systèmes argumentatifs. Sur la base des travaux de Besnard et Hunter, nous avons défini un système d'échange argumentatif entre deux agents capables de générer de nouveaux arguments à partir de contraintes sur leur connaissances exprimées sous la forme d'ensembles X qui leur sont associés. Nous nous concentrons actuellement sur la notion de stratégie argumentative à l'intérieur de ce cadre formel.
Une application générale de nos travaux sur la non-monotonie a lieu dans le cadre ASP (Answer Set Programming).
Enfin, parmi les résultats du projet européen REVIGIS, deux aspects ont émergé sous l’impulsion des chercheurs de INCA en collaboration avec ceux de Toulon : la nécessité d’une formulation initiale solide de la sémantique des variables (ontologie) et le développements de formalismes expressifs et/ou efficaces pour la représentation des préférences et des croyances dans les états épistémiques et une approche pour un choix pertinent selon la sémantique des applications.
Algorithmique pour l'inférence :
Les travaux réalisés ici portent sur les questions d’algorithmique et de complexité relevant de la démonstration automatique, des problèmes de satisfaction de contraintes et d’une de leur généralisation, les problèmes de configuration à base de contraintes. Les formalismes sur lesquels ils s’appuient se situent soit en logique du premier ordre, soit en logique des propositions, ou enfin dans les CSP à domaines finis. Les travaux originellement entrepris au sein de l’équipe ont portés sur les CSP et le problème SAT. Compte-tenu de la difficulté théorique et pratique de ces problèmes du fait de leur NP-complétude, nous avons concentré nos efforts sur l’étude conjointe de classes d’instances de complexité polynomiale, et sur la conception de méthodes et outils de résolution efficaces en pratique. Les principaux fondements théoriques exploités ici portent sur les isomorphismes et sur la notion de décomposition arborescente.
Il est bien connu que la notion de décomposition arborescente de graphes (au sens de Robertson et Seymour), et donc de réseaux de contraintes pour nous, permet de fournir des bornes de complexité théoriques pour la résolution de nombreux problèmes NP-Complet. Une part importante de nos travaux a ainsi porté sur l’exploitation de ce type de caractéristiques structurelles et a conduit à la conception de méthodes de résolution fondées sur les techniques de recherche par énumération (pour l’efficacité pratique des algorithmes classiques basés sur le backtracking et le filtrage par propagation), tout en conservant des propriétés permettant de fournir des bornes de complexité théorique en temps et en espace.
Une autre partie importante de nos travaux a porté sur la recherche et l’exploitation d’isomorphismes ou de symétries dans les jeux de données. En effet, qu’ils soient issus de problèmes réels d’origine industrielle comme ce peut être le cas avec les problèmes de configuration, ou alors qu’ils relèvent de questions d’ordre théorique (cf. recherche de groupes finis en algèbre), de très nombreux jeux de données recèlent des symétries dont la présence accroît significativement le temps de résolution, voire rend celle-ci inconcevable en pratique. Toutefois, leur identification permet d’éviter ce type de phénomène, et peut donc servir à l’optimisation. Les résultats les plus intéressants que nous avons obtenus ici l’ont été à la fois sur certaines applications de la configurations, dont une inattendue au niveau du traitement des langues naturelles, mais aussi dans le cadre de la recherche de groupes finis.
