Dénombrement de modèles en logique équationnelle

De Ensiwiki
Aller à : navigation, rechercher


Dénombrement de modèles en logique équationnelle

Labo LIG
Equipe CAPP
Encadrants Nicolas.Peltier@imag.fr Mnacho.Echenim@imag.fr, Nicolas.Peltier@imag.fr

Thème général

Le problème #SAT consiste, pour une formule propositionnelle en forme normale conjonctive F donnée, à déterminer le nombre de modèles de F. La résolution de ce problème et de son extension à des modèles pondérés a de nombreuses applications dans des domaines tels que l'intelligence artificielle, notamment pour le raisonnement probabiliste.

Contexte du travail

L'équipe CAPP du LIG s'intéresse entre autre à la démonstration automatique et à ses applications dans différents domaines, allant de la vérification de programmes à l'intelligence artificielle.

Sujet

Plusieurs travaux de recherche ont récemment étudié comment les algorithmes de dénombrement pouvaient être étendus à des fragments de la logique du premier ordre. Cependant, les fragments considérés ne tiennent pas compte de l'égalité. Le but de ce projet est d'étudier de quelle façon étendre les algorithmes de dénombrement de modèles à des formules équationnelles.

Références:

Compétences nécessaires

Il est recommandé d'avoir suivi le cours de Fondements de Logique pour l'Informatique en 2A.