Raisonnement automatisé
Le raisonnement automatisé consiste à créer des programmes informatiques qui permettent aux ordinateurs de raisonner complètement, ou presque, automatiquement. Bien que la synthèse automatisée soit considérée comme un sous-domaine de l’intelligence artificielle, elle a également des liens avec l'informatique théorique, voire la philosophie.
Les sous - zones les plus développées de raisonnement automatisé sont théorème automatisé prouvant (et le sous - champ moins automatisé, mais plus pragmatique interactive théorème prouver) et la preuve la vérification automatique (considéré comme raisonnement correct garanti par des hypothèses fixes). Un travail considérable a également été fait dans le raisonnement par analogie induction et enlèvement.
Parmi les autres sujets importants, citons le raisonnement sous incertitude et le raisonnement non monotone . Une partie importante du champ d'incertitude est l'argumentation, où des contraintes supplémentaires de minimalité et de cohérence sont appliquées en plus de la déduction automatisée plus standard. OSCAR de John Pollock est un exemple d'un système d'argumentation automatisé qui est plus spécifique que d’être un simple théorème automatisé prouveur.
Les outils et techniques de raisonnement automatisé incluant les logiques et calculs classiques, la logique floue, l’inférence bayésienne, le raisonnement avec une entropie maximale et de nombreuses techniques ad hoc moins formelles .
