Introduction à la logique informatique - Partie 2 : calcul des prédicats
date_range Starts on February 1, 2016
event_note End date February 15, 2016
assignment Level : Introductive
chat_bubble_outline Language : French
card_giftcard 1 point
Logo My Mooc Business

Top companies choose Edflex to build in-demand career skills.

Get started
Users' reviews
-
starstarstarstarstar

Key Information

credit_card Free access
verified_user Free certificate

About the content

Ce MOOC est la suite de Logique informatique, partie 1.

La logique servait surtout la philosophie et la théologie jusqu'au 19ème siècle. Elle est apparue de manière brutale et cruciale au tournant du 20ème siècle en mathématiques, avec les paradoxes et la question des fondements. Après le théorème de Gödel et la faillite du programme de Hilbert, la logique mathématique est devenue une partie spécialisée des mathématiques pures. Mais l'âge d'or de la logique arrive ensuite avec le développement de l'informatique.

L'utilisation des ordinateurs a forcé à formaliser complètement les problèmes à résoudre; la logique joue un rôle central dans les problèmes de spécification et de vérification des programmes. Du fait d'un lien surprenant entre les preuves et les programmes, la logique est aussi la base de la compréhension des calculs. Plus concrètement, la logique a été à l'origine d'avancées technologiques comme les langages de requêtes dans les bases de données. Beaucoup d'autres liens fondamentaux peuvent être évoqués: avec les circuits, avec la complexité, avec les jeux, avec la linguistique, etc. La logique est omniprésente en informatique.

Après la première partie traitait de calcul propositionnel, cette seconde partie aborde la logique du premier ordre. Aussi appelé calcul des prédicats, c'est le langage dans lequel on exprime la plupart des mathématiques, mais aussi un grand nombre d'applications de la logique en informatique. Retrouvez l'équipe enseignante, ses puzzles favoris et le fameux entscheindungsproblem, pour découvrir la richesse de ce langage!

more_horiz Read more
more_horiz Read less
report_problem

Prerequisite

Ce cours s'adresse à un public large désireux de découvrir la logique informatique: professeurs de mathématiques, étudiants en licence, ingénieurs, etc.

Il est fortement recommandé d'avoir suivi la première partie du MOOC de logique informatique avant de suivre cette deuxième partie.

Dans son ensemble, ce cours ne suppose aucune connaissance spécifique préalable, mais s'adresse cependant à un public ayant une pratique du raisonnement mathématique. Il est souhaitable d'avoir le niveau L2 en mathématiques. Il n'y a aucun pré-requis en informatique.

dns

Syllabus

Semaine 1: introduction, syntaxe et F-algèbres

  1. introduction du cours
  2. syntaxe
  3. F-algèbres

Semaine 2: sémantique

  1. (F-P)-structures
  2. axiomes de l'égalité
  3. exemples de satisfaction

Semaine 3: Skolem et Herbrand

  1. forme prénexe
  2. skolémisation
  3. forme clausale
  4. théorème de Herbrand

Semaine 4: unification et résolution

  1. unification
  2. résolution

Semaine 5: calcul des séquents

  1. calcul des séquent LK1
  2. correction
  3. recherche de preuve
  4. complétude

Semaine 6: perspectives

  1. clauses de Horn
  2. programmation logique
  3. conclusion: ouvertures
record_voice_over

Instructors

David Baelde
Maître de conférences à l'ENS Cachan et chercheur en preuve formelle et sécurité des protocoles au Laboratoire Spécification et Vérification.

Hubert Comon
Professeur à l'ENS Cachan et chercheur en logique et sécurité des protocoles au Laboratoire Spécification et Vérification.

Etienne Lozes
Maître de conférences à l'ENS Cachan et chercheur en logique des programmes et parallélisme au Laboratoire Spécification et Vérification.

store

Content Designer

Université Paris-Saclay

The Université Paris-Saclay (French: Université Paris-Saclay) is a French federal research university which is currently under development. The project is part of the research-intensive and business cluster Paris-Saclay, located near Paris in the Plateau de Saclay. The University of Paris-Saclay is expected to be the training and research center of the Paris-Saclay technology cluster, such as Stanford University in Silicon Valley and the Technion in Israel.

assistant

Platform

FUN

France Université Numérique is the broadcaster of the online courses of French higher education institutions and their partners.

It operates several platforms of diffusion, of which the best known, FUN MOOC, is the first French-speaking academic platform worldwide. Thanks to many partner institutions, this platform offers a vast catalog of courses enriched daily with various themes and current events.

You are the designer of this MOOC?
What is your opinion on this resource ?
Content
0/5
Platform
0/5
Animation
0/5