Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Séance de cours

Sans titre

Concepts associés (22)

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.

Démonstration automatique de théorèmes

La démonstration automatique de théorèmes (DAT) est l'activité d'un logiciel qui démontre une proposition qu'on lui soumet, sans l'aide de l'utilisateur. Les démonstrateurs automatiques de théorème ont résolu des conjectures intéressantes difficiles à établir, certaines ayant échappé aux mathématiciens pendant longtemps ; c'est le cas, par exemple, de la , démontrée en 1996 par le logiciel EQP.