Séance de cours

Logique formelle: preuves et ensembles

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

MATH-113: Algèbre I - structures fondamentales

Le but de ce cours est d'introduire et d'étudier les notions de base de l'algèbre abstraite. ...

Description

Cette séance de cours présente les bases de la logique formelle, en se concentrant sur les expressions logiques, les tautologies et la construction de preuves mathématiques. Il couvre l'importance des preuves formelles, des connecteurs logiques, des quantificateurs et du processus de construction de preuves. Linstructeur souligne la nécessité décrire des preuves strictes et fournit des exemples pour illustrer les concepts.

Enseignant·e·s (2)

Dimitri Stelio Wyss

Enseignement et PhD Doctorant·es actuel·les Elsa Maneval, Mathis Duguin A dirigé les thèses EPFL de Tanguy Vernet, Ilaria Rossinelli Cours Algèbre I - structures fondamentales MATH-113 Le but de ce cours est d'introduire et d'étudier les notions de base de l'algèbre abstraite. Quantum Cohomology MATH-747 Student seminar in pure mathematics MATH-563 L'objectif du séminaire est d'aborder les principaux aspects de la théorie des corps de classes, qui vise à com

Zsolt Patakfalvi

See CV here .

Source officielle

Proximité ontologique

Logique

Logique classique: Calcul des prédicats

Concepts associés (32)

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.

Logique mathématique

La logique mathématique ou métamathématique est une discipline des mathématiques introduite à la fin du , qui s'est donné comme objet l'étude des mathématiques en tant que langage. Les objets fondamentaux de la logique mathématique sont les formules représentant les énoncés mathématiques, les dérivations ou démonstrations formelles représentant les raisonnements mathématiques et les sémantiques ou modèles ou interprétations dans des structures qui donnent un « sens » mathématique générique aux formules (et parfois même aux démonstrations) comme certains invariants : par exemple l'interprétation des formules du calcul des prédicats permet de leur affecter une valeur de vérité'.

Quantification (logique)

vignette|Symboles mathématiques des deux quantificateurs logiques les plus courants.|236px En mathématiques, les expressions « pour tout » (ou « quel que soit ») et « il existe », utilisées pour formuler des propositions mathématiques dans le calcul des prédicats, sont appelées des quantifications. Les symboles qui les représentent en langage formel sont appelés des quantificateurs (ou autrefois des quanteurs). La quantification universelle (« pour tout ... » ou « quel que soit ... ») se dénote par le symbole ∀ (un A à l'envers).

Système formel

Un système formel est une modélisation mathématique d'un langage en général spécialisé. Les éléments linguistiques, mots, phrases, discours, etc., sont représentés par des objets finis (entiers, suites, arbres ou graphes finis...). Le propre d'un système formel est que la correction au sens grammatical de ses éléments est vérifiable algorithmiquement, c'est-à-dire que ceux-ci forment un ensemble récursif.

Conjonction logique

En logique, la conjonction est une opération mise en œuvre par le connecteur binaire et. Le connecteur et est donc un opérateur binaire qui lie deux propositions pour en faire une autre. Si on admet chacune des deux propositions, alors on admettra la proposition qui en est la conjonction. En logique mathématique, le connecteur de conjonction est noté soit &, soit ∧. En théorie de la démonstration, plus particulièrement en calcul des séquents, la conjonction est régie par des règles d'introduction et des règles d'élimination.

Afficher plus

Séances de cours associées (59)

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.

Concept de preuve en mathématiques

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

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.

Introduction & Logique de proposition

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

Propositions en tant que types: Logique et correspondance de programmation

Explore la relation entre les preuves logiques et les preuves de programmation à travers la correspondance de Curry-Howard.

Afficher plus

Concepts associés (32)

Théorie de la démonstration

Logique mathématique

Quantification (logique)

Système formel

Conjonction logique

Afficher plus