Raisonnement automatisé

vignette|Visualisation commune du réseau de neurones artificiels avec puce NOTOC 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. 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 ). Récemment, l'on a proposé le raisonnement continu pour réduire la complexité nécessaire pour analyser des systèmes de large échelle. 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 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. International Joint Conference on Automated Reasoning (IJCAR) Conference on Automat