Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Logique mathématique pour l’informatique P. Clemente INSA Centre Val de Loire L

Logique mathématique pour l’informatique P. Clemente INSA Centre Val de Loire Logique mathématique pour l’informatique Introduction Bibliographie Bibliographie Un livre assez complet sur la logique, pour l’informatique : P. Gochet, P. Gribomont. Logique. Vol. 1 : méthodes pour l’informatique fondamentale, Hermès, 1990. Un ouvrage de référence sur la logique pour l’IA : A. Thayse et coauteurs. Approche logique de l’Intelligence Artiﬁcielle. Vol. 1, Dunod, 1990. Le ouvrage plus récent : N. Jussien Logique(s), langages formels et complexité pour l’informatique, Hermès-Lavoisier, 2006. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 2/260 Logique mathématique pour l’informatique Introduction Bibliographie Outils Le prouver que nous allons utiliser en TD : Prouver 9 (https ://www.cs.unm.edu/ mccune/mace4/) Un prouveur automatique de formule logiques (http ://teachinglogic.liglab.fr/DN/index.php) E Theorem Prover (http ://wwwlehre.dhbw-stuttgart.de/ sschulz/E/Download.html) P. Clemente - INSA Centre Val de Loire Dpt STI 3A 3/260 Logique mathématique pour l’informatique Introduction Une théorie mathématique Qu’est que la logique (mathématique) La logique est un outil formel. On devrait dire les logiques car il en existe une inﬁnité de variantes. La logique utilise les mathématiques comme le font les autres branches des mathématiques, La logique étudie des sortes particulières d’objets mathématiques : les propositions, les théorèmes, les jugements, les démonstrations, etc. Premier constat : la logique est donc une théorie mathématique. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 4/260 Logique mathématique pour l’informatique Introduction Une théorie mathématique La logique pour les mathématiques Comprendre la nature du raisonnement mathématique 1, et la validité de la notion de preuve, d’argumentations, de démonstrations. Faire du “raisonnement” une théorie mathématique comme les autres. Étudier les mathématiques, par les mathématiques. Deuxième constat : la logique applique des mathématiques à des mathématiques. Question : la logique peut-elle s’appliquer à elle-même ? 1. et du raisonnement non mathématique ! P. Clemente - INSA Centre Val de Loire Dpt STI 3A 5/260 Logique mathématique pour l’informatique Introduction Une théorie mathématique La logique pour les informaticiens En informatique, on utilise beaucoup la logique : Mécaniser les processus de raisonnement ; Exemple A et B permet de déduire C ; C et D permet E. ∀x, x = A, B, C, D, E. Posons A = "il pleut", B="je suis dehors", C="je suis mouillé", D="je suis nu", E= j’ai froid" ; et si on a A, B et D qui sont vrais ; Alors, on sait que l’on peut déduire C et E : "je suis mouillé" et "j’ai froid". Exhiber les liens entre démonstrations et calculs ; Formaliser les objets d’un raisonnement par les mathématiques et valider celui-ci par des mathématiques est un calcul. Formaliser les objets informatiques. Voir exemple de vérif. de protocole. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 6/260 Logique mathématique pour l’informatique Introduction Une théorie mathématique La logique pour les informaticiens En informatique, on utilise beaucoup la logique : Mécaniser les processus de raisonnement ; Exemple A et B permet de déduire C ; C et D permet E. ∀x, x = A, B, C, D, E. Posons A = "il pleut", B="je suis dehors", C="je suis mouillé", D="je suis nu", E= j’ai froid" ; et si on a A, B et D qui sont vrais ; Alors, on sait que l’on peut déduire C et E : "je suis mouillé" et "j’ai froid". Exhiber les liens entre démonstrations et calculs ; Formaliser les objets d’un raisonnement par les mathématiques et valider celui-ci par des mathématiques est un calcul. Formaliser les objets informatiques. Voir exemple de vérif. de protocole. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 6/260 Logique mathématique pour l’informatique Introduction Applications Applications directes ou indirectes en informatique Conception de circuits électroniques numériques (algèbre de Boole) ; Vériﬁcation formelle de logiciels (Méthode/langage/atelier B - Méteor) ; Vériﬁcation formelle de protocoles (COQ : philosophes, T = 1) ; Programmation logique (programmation déclarative, n versions de Prolog) ; SGBD déductifs (e.g. Datalog), systèmes experts ; Web Sémantique (RD P. Clemente - INSA Centre Val de Loire Dpt STI 3A 7/260 Logique mathématique pour l’informatique Introduction Applications Démonstration automatique et preuve de théorèmes (parfois jamais démontrés auparavant) ; Programmation sûre formelle : méthode B - atelier B. Simulation de raisonnements en intelligence artiﬁcielle ; Sécurité informatique : traitement automatique de politiques de sécurité ; Traitement automatique de la langue ; Agents intelligents et agents dialoguants. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 8/260 Logique mathématique pour l’informatique Introduction Applications P. Clemente - INSA Centre Val de Loire Dpt STI 3A 9/260 Logique mathématique pour l’informatique Introduction Applications François Fages 25 ans du LIFO, Orléans, 14/03/12 Formal Reaction Rules Complexation: A + B => A-B. Decomplexation A-B => A + B. cdk1+cycB => cdk1±cycB Phosphorylation: A =[K]=> A~{p}. Dephosphorylation A~{p} =[P]=> A. Cdk1-CycB =[Myt1]=> Cdk1~{thr161}-CycB Cdk1~{thr14,tyr15}-CycB =[Cdc25~{Nterm}]=> Cdk1-CycB Synthesis: _ =[G]=> A. Degradation: A =[C]=> _. _ =[#E2-E2f13-Dp12]=> RNAcycA Transport: A::L1 => A::L2. RNAcycA::nucleus => RNAcycA::cytoplasm Cdk1~{p}-CycB::cytoplasm => Cdk1~{p}-CycB::nucleus P. Clemente - INSA Centre Val de Loire Dpt STI 3A 10/260 Logique mathématique pour l’informatique Introduction Applications P. Clemente - INSA Centre Val de Loire Dpt STI 3A 11/260 Logique mathématique pour l’informatique Introduction Applications P. Clemente - INSA Centre Val de Loire Dpt STI 3A 12/260 Logique mathématique pour l’informatique Introduction Applications http ://www.irisa.fr/celtique/genet/Crypt/cours.pdf P. Clemente - INSA Centre Val de Loire Dpt STI 3A 13/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Chapitre 1. Logique Propositionnelle P. Clemente - INSA Centre Val de Loire Dpt STI 3A 14/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction Plan : Chapitre 1. Logique Propositionnelle Introduction Syntaxe Sémantique Algorithmique Équivalence et dualité de formules Représentation canonique Algorithme de Davis et Putnam Technique de résolution Système formel, déduction et démonstration P. Clemente - INSA Centre Val de Loire Dpt STI 3A 15/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction Introduction La logique des propositions permet de représenter des propositions simples, des faits du monde, tels que : « x est un lièvre » et « y est une tortue » ; ou des propositions conditionnées ou paramétrées : « si x est arrivé, alors x est parti » ; « si x et y sont partis en même temps alors y arrivera avant x ». P. Clemente - INSA Centre Val de Loire Dpt STI 3A 16/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction Dans la logique des propositions, les variables ne prennent que deux valeurs Vrai (V), Faux (F). Une variable propositionnelle correspond à une variable de type booléen en Pascal, ADA, ... On ne traite donc, dans le calcul des propositions, que des expressions booléennes. Le calcul des propositions est un modèle mathématique qui permet de raisonner sur la nature vraie ou fausse des expressions logiques. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 17/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction On distingue la syntaxe (règles d’écriture des formules) et la sémantique (interprétation des formules). Les formules peuvent être syntaxiquement représentées par des suites de symboles ou par des arbres. Le calcul des propositions traite du raisonnement sur les propositions indépendamment de leur sens. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 18/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction Énoncés en langue naturelle Une proposition est un énoncé qui peut être vrai ou faux. En arithmétique : 1 + 1 = 2 est une proposition vraie 0 > 1 est une proposition fausse Certains énoncés sont des propositions mais nous ne savons pas si elles sont vraies ou fausses, c’est le cas de certaines conjectures mathématiques ni démontrées ni invalidées. Certains énoncés ne sont pas des propositions (i.e., ni vrai, ni faux) : "cet énoncé est faux" ; "taisez-vous" ; "c’est ﬁni ?". P. Clemente - INSA Centre Val de Loire Dpt STI 3A 19/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction Vérité de langage Considérons l’énoncé suivant : "Un quart d’heure avant sa mort, il était encore en vie." Pour déterminer l’exactitude de cet énoncé, il suﬃt de connaître le sens des mots, cet énoncé est une vérité de langage. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 20/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction Vérité de fait Considérons l’énoncé suivant : "La Terre tourne" Cet énoncé n’est pas une vérité de langage, car il exprime un fait [quasiment] inconditionnel. Cet énoncé est une vérité de fait. P. Clemente - INSA Centre Val de Loire Dpt STI 3A 21/260 Logique mathématique pour l’informatique Chapitre 1. Logique Propositionnelle Introduction Vérité logique Considérons enﬁn l’énoncé suivant : "[Si il se fait que] si il pleut, (alors) la route est mouillée, [alors il se fait que] si la route n’est pas mouillée, (alors) il ne pleut pas." Pour admettre ce second énoncé, il faut : connaître le sens de certains connecteurs logiques (si ... alors, ne ... pas) et de savoir que les morceaux de phrase restant ("il pleut" et "la route est mouillée") sont des uploads/Philosophie/ cours-logique.pdf