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

Flyspeck II : Les programmes linéaires de base

Description

Cette séance de cours couvre le projet Flyspeck II, en mettant l'accent sur les programmes linéaires de base et la bibliothèque d'informatique HOL. Il traite de l'histoire de la conjecture de Kepler, des défis à relever pour certifier l'exactitude de la preuve et de l'architecture de la HCL. La séance de cours souligne l'importance d'une certification rigoureuse dans les documents mathématiques.

Source officielle

Concepts associés (22)

Standard ML

Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers. Standard ML is a modern dialect of ML, the language used in the Logic for Computable Functions (LCF) theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML.

OCaml

OCaml, anciennement connu sous le nom d'Objective Caml, est l'implémentation la plus avancée du langage de programmation Caml, créé par Xavier Leroy, Jérôme Vouillon, , Didier Rémy et leurs collaborateurs en 1996. Ce langage, de la famille des langages ML, est un projet open source dirigé et maintenu essentiellement par l'Inria. OCaml est le successeur de Caml Light, auquel il a ajouté entre autres une couche de programmation objet.

Optimisation linéaire

thumb|upright=0.5|Optimisation linéaire dans un espace à deux dimensions (x1, x2). La fonction-coût fc est représentée par les lignes de niveau bleues à gauche et par le plan bleu à droite. L'ensemble admissible E est le pentagone vert. En optimisation mathématique, un problème d'optimisation linéaire demande de minimiser une fonction linéaire sur un polyèdre convexe. La fonction que l'on minimise ainsi que les contraintes sont décrites par des fonctions linéaires, d'où le nom donné à ces problèmes.

Sous-programme

En informatique, un sous-programme est un sous-ensemble du programme dans sa hiérarchie fonctionnelle. Un sous-programme doit pouvoir mémoriser l'adresse du code appelant pour permettre, à l'aide d'une instruction spécifique, de charger le pointeur de programme avec cette adresse de retour. Cela correspond bien souvent à une routine. Cependant, la notion de sous-programme est un peu plus générale, car il ne possède pas nécessairement son propre espace de noms. C'est le cas par exemple des sous-programmes appelés par l'instruction en BASIC.

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.

Afficher plus

Séances de cours associées (28)

Programmation linéaire : correspondance bipartite pondérée

Couvre la programmation linéaire, la correspondance bipartite pondérée et les problèmes de couverture de sommet en optimisation.

Algorithmes d'approximation

Couvre les algorithmes d'approximation pour les problèmes d'optimisation, la relaxation LP et les techniques d'arrondi aléatoire.

Architecture et société: Innovations, Critique et Résistance

Explore le rôle de l'architecture et des architectes dans la société moderne, en se demandant si les architectes peuvent façonner la société ou si l'architecture est déterminée par les conditions sociales, politiques et économiques.

Signification en architecture: Aldo van Eyck, Denise Scott Brown

Explore les philosophies architecturales d'Aldo van Eyck et de Denise Scott Brown, mettant l'accent sur la création d'un sens bâti et l'intégration des expériences passées dans les conceptions actuelles.

Architecture moderne et climat

Explore la relation entre l'architecture moderne et la science du climat, en mettant l'accent sur l'optimisation de l'environnement bâti pour les conditions climatiques.

Afficher plus

Concepts associés (22)

Standard ML

OCaml

Optimisation linéaire

Sous-programme

Démonstration automatique de théorèmes

Afficher plus