Retour site Christian Retoré

14 JANVIER 2019


1ST WORLD LOGIC DAY
PREMIERE JOURNEE MONDIALE DE LA LOGIQUE 

UNIVERSITE DE MONTPELLIER, POLYTECH, LUNDI 14 JANVIER 2019, 15:00

SITE http://www.lirmm.fr/~retore/WLD/WorldLogicDay.html


A l’occasion de la première journée mondiale de la logique http://www.logica-universalis.org/wld
le 14 janvier 2019  (jour de la naissance d’Alfred Tarski et de la mort de Kurt Gödel, suivant une idée de J.-Y. Beziau) 
nous proposons, à Montpellier, quelques exposés de vulgarisation scientifique.  

LUNDI 14 JANVIER  2019 15:00-19:00 Salle SC 001 Polytech (bâtiment 31), Campus Triolet (campus sciences), Université de Montpellier 

plan du campus sciences Triolet

plan du batiment 31 Polytech


15:00  UNE HISTOIRE DE LA LOGIQUE MATHEMATIQUE: DE LA PHILOSOPHIE A L'INFORMATIQUE 
Christian Retoré,
LIRMM, Université de Montpellier, CNRS, Montpellier, France
 
16:00  VÉRITÉ VERSUS VALIDITÉ À LA LUMIÈRE DE LA MÉTHODOLOGIE DES SCIENCES DÉDUCTIVES DE TARSKI
Viviane Durand-Guerrier, IMAG,
Université de Montpellier, CNRS, Montpellier, France

17:00 LA LOGIQUE DANS LE DEBAT PUBLIC
Jean Sallantin
LIRMM, Université de Montpellier, CNRS, Montpellier, France

18:00 DEMO DU LOGICIEL DE DECOUVERTE DE LA LOGIQUE
« LOGICAL MYSTERIES » DE CHRISTOPHER DARTNELL (VIDEO DE OLIVIER ROIZES)
Jean Sallantin LIRMM, Université de Montpellier, CNRS, Montpellier, France

18:15  PROUVER UN PROGRAMME, ÇA VEUT DIRE QUOI ? 
David Delahaye,
LIRMM, Université de Montpellier, CNRS, Montpellier, France

19H FIN

Résumés ci-dessous.


UNE HISTOIRE DE LA LOGIQUE MATHEMATIQUE : DE LA PHILOSOPHIE A L'INFORMATIQUE

D’Aristote à la scolastique, la logique fut placée au commencement des études et traités de philosophie, 
afin que le philosophe raisonne sur tout sujet avec une rigueur comparable à celles des mathématiques. 
En dépit de quelques contributions isolées, il faut attendre la fin du XIXe, avec le questionnement 
sur les fondements et la cohérence des mathématiques, 
pour que la logique se renouvelle et revienne au premier plan de la scène scientifique. 
     Ce mariage entre logique et mathématique a évidemment connu des succès en mathématiques, 
mais il a aussi intensément contribué au développement de la notion de calcul et de l’informatique, 
dès la seconde guerre mondiale, en raison des liens entre décidabilité et calculabilité.
Nous retracerons le développement de la logique mathématique au XXe siècle, 
nous nous pencherons plus particulièrement sur la notion de calcul et de preuve formelle.


VÉRITÉ VERSUS VALIDITÉ À LA LUMIÈRE DE LA MÉTHODOLOGIE DES SCIENCES DÉDUCTIVES DE TARSKI

Dans sa quête d'une définition sémantique de la la vérité, Tarski introduit deux notions très simples qui vont se révéler très fécondes:
la notion de satisfaction d'une phrase ouverte par un élément de l'univers du discours 
et la notion de modèle d'une formule dans un domaine d'interprétation donné.
ceci est au coeur de la méthodologie des sciences déductives qui articule syntaxe et sémantique 
et permet de clarifier les relations entre vérité dans une interprétation et validité logique. 
Après avoir présenté les principaux aspects de cette élaboration, j’illustrerai sur un exemple simple la fécondité de cette approche.


LA LOGIQUE DANS LE DEBAT PUBLIC

Pour Aristote, la logique était une arme pour se défendre des beaux parleurs, qu’en est-il aujourd’hui dans les débats sciences/sociétés.
Peut-on fonder sur la logique la confiance la participation et la créativité des débats.


PROUVER UN PROGRAMME, ÇA VEUT DIRE QUOI ?

En Informatique, certains systèmes sont dits critiques en ce sens qu'un bug informatique peut provoquer 
une défaillance du système dont les conséquences peuvent être potentiellement catastrophiques (pertes humaines, 
pertes financières, conséquences graves pour l'environnement, etc.). Ainsi, le développement 
de ces systèmes nécessitent l'utilisation de méthodes spécifiques permettant d'assurer la production de logiciels sûrs. 
Ces méthodes sont appelées méthodes formelles.

Parmi ces méthodes, il y a en particulier les méthodes déductives reposant principalement sur l'utilisation de la logique, 
et appelées également preuve de programme. L'idée consiste à spécifier formellement le comportement du programme 
au moyen de la logique et à faire une preuve que le programme est conforme à cette spécification.

Cet exposé s'adresse essentiellement aux curieux qui veulent comprendre 
sur des exemples simples les différents principes cachés derrière la preuve de programme.



Retour site Christian Retoré