Raisonnement automatisé

Le raisonnement automatisé est un domaine de l'informatique consacré à la compréhension des différents aspects du raisonnement de manière à permettre la création de logiciels qui permettraient aux ordinateurs de « raisonner » de manière automatique, ou presque. Il est considéré habituellement comme un sous-domaine de l'intelligence artificielle, mais possède aussi de fortes connexions avec l'Informatique théorique et même avec la philosophie.

Visualisation commune du réseau de neurones artificiels avec puce

Les sous-domaines les plus développés du raisonnement automatisé sont probablement l'assistant de preuve (qui en pratique se trouve être plus pragmatique mais moins automatisé que sa théorie), la démonstration automatique de théorèmes et la vérification de preuve (procédé qui garantit un raisonnement correct en se basant sur l'axiome selon lequel les hypothèses fournies sont justes^{[réf. souhaitée]}). Recemment, l'on a proposé le raisonnement continu pour réduire la complexité nécessaire pour analyser des systèmes de large echélle. Cependant, un travail énorme a été fourni dans le raisonnement par analogie, induction et abduction. D'autres sujets importants sont aussi le raisonnement sous les contraintes de l'incertitude et le raisonnement non-monotone. Une partie importante du raisonnement sous la contrainte de l'incertitude est l'argumentation, sous des contraintes de minimalité et de cohérence, appliquée au sommet des déductions automatisées tout ce qu'il y a de plus standard. Le système d'Oscar de John Pollock (en) est un exemple d'argumentation automatisée bien plus spécifique qu'un « simple » assistant de preuve de théorème. L'argumentation formelle est un sous-domaine de l'intelligence artificielle.

Les outils et techniques du raisonnement automatisé incluent les logiques et les calculs classiques de la preuve automatique de théorème, mais aussi la logique floue, l'inférence bayésienne, le raisonnement par le principe d'entropie maximale et un grand nombre de techniques ad-hoc moins formelles.