Séance de cours

Flyspeck II : Les programmes linéaires de base

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

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 (23)

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.

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.

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 (38)

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.

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.

Architecture et société: Innovations, Critique et Autonomie

S'insère dans la relation complexe entre l'architecture et la société, explorant les possibilités de créer des designs architecturaux autonomes et critiques.

Théorie architecturale : intention ou interprétation

S'insère dans le débat entre l'intention de l'auteur et l'interprétation du critique en théorie architecturale, explorant ses implications pour l'architecture contemporaine.

Techniques de programmation linéaire dans l'apprentissage par renforcement

Couvre l'approche de programmation linéaire de l'apprentissage par renforcement, en se concentrant sur ses applications et ses avantages dans la résolution des processus décisionnels de Markov.

Afficher plus

Concepts associés (23)

OCaml

Standard ML

Optimisation linéaire

Sous-programme

Démonstration automatique de théorèmes

Afficher plus