Séances de cours associées à Calcul proposé

Plonge dans le concept de preuve en mathématiques, en soulignant l'importance de la preuve et du raisonnement logique.

Énumérabilité récursive: Machines de Turing et langages indécidables

Couvre les langages énumérables récursivement, les machines de Turing et la construction de langages indécidables.

Couvre les bases de la logique de proposition, des connectifs logiques, des tables de vérité et des propositions composées.

Complexité et induction: Algorithmes et preuves

Couvre la complexité, les algorithmes et les preuves du pire cas, y compris l'induction mathématique et la récursion.

Coq: Introduction

Présente Coq, couvrant la définition des propositions, la démonstration des théorèmes, et l'utilisation de tactiques.

Preuves et calculs : un voyage à travers la théorie mathématique

Explore les preuves mathématiques historiques, les problèmes de décision, les systèmes de déductibilité, les preuves probabilistes et quantiques, et les systèmes de preuve interactifs.

Raisonnement automatisé : vérification formelle avec LISA

Examine la vérification formelle à l'aide de l'assistant d'épreuve LISA et du vérificateur d'équivalence OCBSL.

Complexité computationnelle: Théorie et applications

Explore la complexité computationnelle, l'exhaustivité du NP et les réductions polynômes de l'informatique théorique.

Preuves formelles: vérification des invariants et des modèles liés

Explore les preuves formelles, les problèmes de satisfaisabilité et les invariants inductifs en utilisant des requêtes SAT dans des circuits séquentiels.

Fonctions d'injection : propriétés et exemples

Couvre les propriétés des fonctions injectives et démontre leurs preuves à travers des exemples et des aides visuelles.

Théorie des ensembles : introduction et opérations

Couvre les fondements des mathématiques à travers des concepts de théorie des ensembles tels que l'adhésion et les syndicats.

Logique proposée: Traductions et équivalences

Couvre la traduction du langage naturel en logique de proposition et la démonstration de tautologies.

Physique statistique: Lunettes de spin et optimisation

Explore le modèle Curie-Weiss, les lunettes de spin et les problèmes d'optimisation en physique statistique.

Ensembles et opérations: Introduction aux mathématiques

Couvre les bases des ensembles et des opérations en mathématiques, des propriétés des ensembles aux opérations avancées.

Produit cartésien en algèbre linéaire

Explore le produit cartésien en algèbre linéaire et la méthode d'induction pour prouver des propositions.

Éléments de complexité computationnelle

Introduit la complexité computationnelle, les problèmes de décision, la complexité quantique et les algorithmes probabilistes, y compris les problèmes dures au NP et les problèmes complets au NP.

Structure logique: principes de choix et d'induction de barre

Couvre la structure logique des principes équivalents au choix et à l'induction de barre, en se concentrant sur le choix dépendant généralisé et ses implications en mathématiques.

Preuves : Logique, Mathématiques et Algorithmes

Explore les concepts, les techniques et les applications de la preuve dans la logique, les mathématiques et les algorithmes.

Logique formelle: preuves et ensembles Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre les bases de la logique formelle, en se concentrant sur les expressions logiques et les preuves mathématiques.

Hoare Logic: Fondements et applications Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre Hoare Logic, ses fondements, ses applications et son importance dans la vérification des programmes.