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

Concept

Raisonnement automatisé

Séances de cours associées (32)

Raisonnement automatisé dans la pratique

Explore les systèmes de raisonnement automatisés pratiques comme TPTP, TSTP et CASC, en soulignant l'importance de la cohérence et des développements futurs.

Intelligence Artificielle Fondamentaux

Couvre les bases de l'intelligence artificielle, en mettant l'accent sur les applications pratiques et les exercices de programmation.

Vérification formelle et synthèse des programmes

Par l’instructeur Viktor Kuncak explore les activités de vérification formelle, de synthèse de programme et d’enseignement à l’EPFL.

Nouvelles technologies en matière de recrutement

Explore l'impact des nouvelles technologies sur le recrutement, en soulignant l'importance d'outils justes et précis.

Rechercher Algorithmes: Raisons Abductives

Explore le raisonnement abducteur, les algorithmes de recherche et la recherche heuristique pour la résolution de problèmes.

Logique des prédicats : bases et applications

Couvre les bases et les applications de la logique des prédicats, y compris les quantificateurs, les prédicats et les fonctions propositionnelles.

Systèmes de règles, simulations et mondes parallèles

Plongez dans les systèmes de règles, les simulations et les mondes parallèles, en explorant Prolog, les algorithmes de retour en arrière, la complexité logique, la simulation Game of Life et le concept de Simulats.

Croyances : Définition et mécanismes

S'insère dans la définition des croyances, l'influence sur le comportement, la classification et la relation avec la science.

Convergence d'une séquence définie de façon récursive MOOC: Analyse I MOOC: Analyse I (partie 3) : Suites de nombres réels I et II

Explore la convergence des séquences définies par la récursion et le raisonnement mathématique qui la sous-tend.

Planification automatisée : modélisation et contraintes

Explore la planification automatisée, les contraintes et les applications dans divers domaines, en mettant l'accent sur les défis et l'efficacité de la résolution des problèmes de planification.

Sans titre

Induction pour les solvants SMT

Explore les techniques d'induction dans les résolveurs SMT, en mettant l'accent sur l'implémentation de CVC4 et la performance compétitive avec d'autres proverbes.

Sans titre

Entreprises : Politiques des ressources humaines

Plonge dans l'impact des nouvelles technologies sur les processus de recrutement et de sélection dans les entreprises, en insistant sur la nécessité de prévoir le rendement futur du travail.

La loi des grands nombres : preuves et applications

Explore la preuve et les applications de la loi des grands nombres, en mettant l'accent sur la convergence de la distribution empirique.

Vérification formelle et synthèse des programmes

Explore les recherches de Viktor Kuncak sur la vérification formelle, la synthèse de programmes et les activités d'enseignement à l'EPFL.

Introduction à l'élimination des quantificateurs pour l'arithmétique de Presbourg

Introduit une méthodologie de vérification formelle et l'arithmétique de Presburger pour la vérification de programme et le raisonnement automatisé.

Algèbre linéaire : fonctions injectives

Explore les fonctions d'injection en algèbre linéaire, démontrant comment prouver l'injectivité étape par étape.

Intégration par récurrence MOOC: Analyse I MOOC: Analyse I (partie 7) : Intégrales indéfinies et définies, intégration (chapitres choisis)

Explore l'intégration par la méthode de récurrence avec des exemples de racines carrées et de polynômes.

Tutoriel du système de vérification inoxydable

Introduit Stainless, un outil open-source pour vérifier les programmes Scala, couvrant le langage, la modélisation, les conseils de vérification et les travaux intérieurs.