Remerciez-le!

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

logiquepropositionnelle

Leçon Formule du calcul propositionnel représentation forme normale satis ?abilité Applications Julie Parreaux - Références pour la leçon Duparc La logique pas à pas Cori et Lascar La logique mathématique tome Stern Fondements mathématiques de l ? informatique Transformation de Tseitin Développements de la leçon -SAT est NL-complet donc dans P Plan de la leçon Le langage de la logique propositionnelle Syntaxe p Représentations Sémantique p Théories et preuves Équivalence de formules Équivalence sémantique et équisatis ?abilité p Systèmes de connecteurs Formes normales conjonctives ou disjonctives Résoudre la satis ?abilité en pratique Considérer des fragments de la logique Essayer de résoudre astucieusement Motivation Défense La logique propositionnelle est une logique très simple permettant d ? exprimer des contraintes c ? est la première logique que nous utilisons CCe qu ? en dit le jury Le jury attend des candidats qu ? ils abordent les questions de la complexité de la satis ?abilité Pour autant les applications ne sauraient se réduire à la réduction de problèmes NPcomplets à SAT Une partie signi ?cative du plan doit être consacrée à la représentation des formules et à leurs formes normales Le langage de la logique propositionnelle On formalise la logique gr? ce à une syntaxe une sémantique et un lien entre les deux donné par un système de preuve sur la syntaxe Nous allons également donner plusieurs représentations possibles dans un ordinateur de la syntaxe Syntaxe p ?? Dé ?nition langage avec connecteurs minimaux induction exemples ?? Notation Autres connecteurs ?? Remarque Ambigu? té et parenthèses exemples Représentations Comment on représente les mots de ce langage dans un ordinateur Laquelle est la plus ef ?cace sous quels critères ?? Représentation linéaire ?? Représentation arborescente fait appara? tre l ? induction Théorème de la lecture unique p unicité de la représentation par l ? arbre représentation fortement non ambigu? ?? Représentation DAG direct acyclique graph moins de mémoire utilisé pour la satis- ?abilité ?? Représentation BD ?? Représentation circuit donne de nouvelles classes de complexités Sémantique p Comment donner du sens à ce qu ? on écrit Que signi ?e ces formules ?? Valuation sur un modèle ?? Application traduction du langage naturel ?? Problèmes validité et satis ?abilité deux notions duales ?? Une représentation table de vérité c ? est une méthode pratique ordonnée pour tester la validité d ? une formule ?? Remarque complexité de calcul Conséquence de Cook ?? Théorème Cook ?? Application réduction de problème pour NP-dureté problème de séparation des auto- mates ?? Dé ?nition tautologie contradictions C Théories et preuves Véri ?er que nous n ? avons pas fait n ? importe quoi avec ces dé ?nitions ?? Dé ?nition théorie ?? Théorème compacité ?? Applications coloriage de sous-graphe pavage logique du premier ordre ?? Dé ?nition CNF on voit après comment la mettre sous forme normale résolution ?? Théorème correction et complétude Les autres logiques ?? Taille des arbres et certi ?cats Équivalence de formules A ?n de trouver des moyens de résoudre le problème de satis