Séance de cours

Techniques de programmation logique: Recherche et unification automatisées de preuves

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.

Dans cours (2)

CS-428: Interactive theorem proving

A hands-on introduction to interactive theorem proving, computer-checked mathematics, compiler verification, proofs as programs, dependent types, and proof automation. Come learn how to write computer-checked proofs and certified bug-free code! ...

CS-628: Interactive Theorem Proving CS

A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code! ...

Description

Cette séance de cours présente des concepts de programmation logique, en se concentrant sur les techniques de recherche de preuves automatisées dans LTAC, les variables existentielles et l'unification. L'instructeur commence par discuter des fonctionnalités de base de LTAC pour la recherche de preuve automatique, soulignant l'importance des variables existentielles dans la programmation logique. La séance de cours progresse vers le concept d'unification, en expliquant comment il joue un rôle crucial dans la programmation logique et la construction de la preuve. L'instructeur fournit des exemples de définition des relations inductives, en particulier la fonction d'addition, et montre comment prouver des équivalences entre différentes définitions. La séance de cours couvre également les techniques de preuve avancées, y compris l'utilisation de tactiques telles que l'auto et l'eauto pour simplifier les preuves. L'instructeur met l'accent sur l'importance de comprendre les principes sous-jacents de la recherche de preuves et l'application de la tactique dans Coq. Tout au long de la séance de cours, divers exemples sont présentés pour illustrer l'application pratique de ces concepts dans la programmation logique, aboutissant à une discussion sur la synthèse des programmes et l'évaluation des expressions dans Coq.

Source officielle

Concepts associés (32)

Assistant de preuve

En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques. Beaucoup de projets ont été lancés pour formaliser les mathématiques, en 1966, Nicolaas de Bruijn lance le projet Automath, suivi par d'autres projets.

XEmacs

XEmacs is a graphical- and console-based text editor which runs on almost any Unix-like operating system as well as Microsoft Windows. XEmacs is a fork, based on a version of GNU Emacs from the late 1980s. Any user can download, use, and modify XEmacs as free software available under the GNU General Public License version 2 or any later version. Between 1987 and 1993 significant delays occurred in bringing out a new version of GNU Emacs (presumed to be version 19). In the late 1980s, Richard P. Gabriel's Lucid Inc.

Théorie de la démonstration

La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du . Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au congrès international des mathématiciens en 1900 avec pour objectif de démontrer la cohérence des mathématiques.

Coq (logiciel)

Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l’Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon). Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand.

Agda (programming language)

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is also a proof assistant based on the propositions-as-types paradigm, but unlike Coq, has no separate tactics language, and proofs are written in a functional programming style.

Afficher plus

Séances de cours associées (64)

Introduction à Coq: Expressions arithmétiques et évaluateurs

Couvre les bases de Coq, en se concentrant sur les expressions arithmétiques, l'évaluation et les techniques de preuve.

Sémantique à grande échelle : définition d'expressions et de commandes arithmétiques

Couvre la définition d'un langage de programmation simple et sa sémantique à grande échelle, y compris les expressions arithmétiques et les commandes impératives.

Propositions inductives : comprendre l’évaluation dans Coq

Couvre les propositions inductives en Coq, en se concentrant sur les règles dévaluation pour les expressions arithmétiques et leurs applications dans la définition des fonctions partielles et non déterministes.

Atelier Coq: Types de données inductives et preuves

Couvre la définition d'un type de données inductives dans Coq et la façon de construire des preuves de manière interactive en utilisant des tactiques.

Introduction aux scripts de preuve: bases de Ltac

Présente les bases du script de preuve en Coq, en se concentrant sur le langage Ltac et ses tactiques pour gérer efficacement les preuves.

Afficher plus

Concepts associés (32)

Assistant de preuve

XEmacs

Théorie de la démonstration

Coq (logiciel)

Agda (programming language)

Afficher plus